lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
We should move all `*Info.format` functions to `MessageData` instead so options like `pp.raw` and `pp.raw.showInfo` are heeded correctly.
The function `IndPredBelow.mkBelow` fails to generate `brecOn` for the following inductive predicate. ```lean set_option trace.Meta.IndPredBelow true in inductive TransClosure (r : α → α → Prop) : α → α...
```lean macro (priority := high) "let " x:ident : tactic => `(let' $x := ?_) example : True := by let x exact Nat -- expected ':=' or '|' ```...
```lean import Lean #check elabTermEnsuringType --^ textDocument/completion ``` returns no result, even though the document symbols (ctrl-T) request does reveal `Lean.Elab.Term.elabTermEnsuringType` and `Lean.Elab.Tactic.elabTermEnsuringType`. This is a regression compared to lean...
This came up in context of #1647: an implicit auto-param could only be specified using a named argument of `@`
As in Lean 3, declaration names starting with `_` should be rejected.
```lean example : True := by { skip; trivial } ``` fails with a parse error unless the indentation of `trivial` is greater or equal to the column of `skip`....
```lean example : ∀ (l : List α) n, l.get? n = some a → True | _::_, _+1, _ => trivial | _::_, 0, rfl => trivial --^ unused...
* In a few contexts, it would be helpful if in addition to `Init` another file can be loaded before each file. * This can be a command-line option *...
Dot notation for functions does not behave in an expected way when there are type families. For example, if we define a dependent `Function.swap` function, we might expect (or at...
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover