Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
I keep messing things up, so time for some guard rails, so check them using [actionlint](https://github.com/raven-actions/actionlint). This also runs [shellcheck](https://www.shellcheck.net/) on the files. Shellcheck is a bit picky about putting double quotes around variables, and will flag many cases where we know it’s safe, but why not simply always write the safer variant. Unfortunately, actionlint does not (yet) check `actions/github-script` scripts, which is unfortunate. Maybe they will in the future (https://github.com/rhysd/actionlint/issues/389) |
||
|---|---|---|
| .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.
We provide nightly releases and have just begun regular stable point releases.
About
- Quickstart
- Walkthrough installation video
- Quick tour video
- 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.