Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
f986f69a32
This bug is the real cause of leanprover/vscode-lean4#392. At the end of a tactic state, the client calls `getInteractiveDiagnostics` with a range `[last line of proof, last line of proof + 1)`. The `fullRange` span of the `unresolved goals` error however is something like `[(first line of proof, start character), (last line of proof, nonzero end character)). Since it operates on line numbers, `getInteractiveDiagnostics` would then check whether `[last line of proof, last line of proof + 1)` and `[first line of proof, last line of proof)` intersect, which is false because of the excluded upper bound on the latter interval, despite the fact that the end character in the last line may be nonzero. This fix adjusts the intersection logic to use `[first line of proof, last line of proof]` if the end character is nonzero. Closes leanprover/vscode-lean4#392. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| default.nix | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
| shell.nix | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Manual
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
- FAQ
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.