Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
69c71f6476
Some eliminators (such as `False.rec`) have an explicit motive argument. The `elabAsElim` elaborator assumed that all motives are implicit. If the explicit motive argument is `_`, then it uses the elab-as-elim procedure, and otherwise it falls back to the standard app elaborator. Furthermore, if an explicit elaborator is not provided, it falls back to treating the elaborator as being implicit, which is convenient for writing `h.rec` rather than `h.rec _`. Rationale: for `False.rec`, this simulates it having an implicit motive, and also motives are generally not going to be available in the expected type. Closes #4347 |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .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
- 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 (documentation source: doc/make/index.md).