Mario Carneiro
Mario Carneiro
> @digama0 We do believe that moving Mathlib's linters into a separate library (in the same repo) is achievable and independently valuable (for downstream users as well). This is likely...
> do we need a specific opt-out in the vscode-lean4 or is the generic one sufficient? It definitely needs an opt out (I personally dislike inlay hints because of the...
Isn't it possible to use `notFollowedBy` to parse the `&&` in this case, instead of using high precedence (which would also affect `if let x := then e1 else e2`)?
um, that's the name of a very popular function on `Bool`...
Grepping for it (which is hard...) reveals some uses in inductive types denoting formula syntax. `and` is a pretty high-demand identifier name.
`rec` is also a pseudo-keyword, right? Can we do something like that, say that `and` is not legal unparenthesized inside the condition of an if let statement? That's a *much*...
I'm not totally against it, but it would need some publicity on zulip first I think to get people on board with the idea. I expect that for a lot...
I mean mathematicians. I use `if let` all the time, and I would use `if let` chains if they were available, but if you are spending your time doing proofs...
Unfortunately, that syntax overlaps with regular `let` expressions inside the conditional. That is, `if let x := a; b then c else d` is already valid syntax and means `if...
> The induction principle we would want is > > ``` > axiom foo.induct_better (motive : Nat → Prop) (case1 : motive 0) > (case2 : ∀ (n : Nat),...