Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
https://live.lean-lang.org/#project=lean-nightly now allows users to play around with the latest lean nightly, and it seems prudent to ask them to test bug reports, if possible, there, and not just with whatever release they use. Also reformatted the descriptions to look well in a text area. Users will not see this as rendered markdown, but as plain text. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| 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).