lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
### Description In the following unfinished proof: ```lean example : ∃n, n < 1 := by have h : 0 < 1 := --^ cursor here exact ⟨0, h⟩ ```...
(as created by `mklink` or cmake using Developer Mode)
### Prerequisites * [ ] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues)....
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues). *...
If there are two different files that contain declarations with the same name, the go to definition feature will sometimes jump to the declaration in the wrong file. This seems...
Motivation: examples such as https://github.com/leanprover/lean4/blob/master/tests/lean/run/nestedInductiveRecType.lean In this example, `T` is a nested inductive type. So, in the current implementation, any recursive function is defined using well-founded recursion. However, functions defined...
Lean 3 has this feature. It has performance problems and limitations.
There have been multiple discussions about the structure of our documentation recently. There is also a practical issue of the chapter sidebar becoming too long to comfortably navigate the mdBook...
### Description There does not seem to be a `pp` option which would make the delaborator put in names of non-dependent binders when they do not contain macro scopes (so...
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover