Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
81fe3b6d05
This PR changes the "declaration uses 'sorry'" error to pretty print an actual `sorry` expression in the message. The effect is that the `sorry` is hoverable and, if it's labeled, you can "go to definition" to see where it came from. The implementation prefers reporting synthetic sorries. These can appear even if there are no error messages if a declaration refers to a declaration that has elaboration errors. Users should focus on elaboration errors before worrying about user-written `sorry`s. In the future we could have some more precise logic for sorry reporting. All the sorries in a declaration should be considered to be reported, and we should not re-report sorries in later declarations. Some elaborators use `warn.sorry` to avoid re-reporting sorries in auxiliary declarations. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.