Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
79428827b8
Adds an optional `text` argument to the `fetchFile*` and `buildFile*` definitions that can be used to hash built files as text files (with normalized line endings) instead of as binary files (the previous default). Separately, this change also significantly expands the documentation in the `Lake.Build.Trace` module and preforms minor touchups of some build job signatures. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| debug.log | ||
| 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).