Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
66e0a5440b
This PR augments the Lake configuration data structures declarations (e.g., `PackageConfig`, `LeanLibConfig`) to produce additional metadata which is used to automatically generate the Lean & TOML encoders and decoders via metaprograms. **Warning:** This refactor should not produce any significant user-facing breaking changes. However, configurations have been tweaked, so there is a chance something may have slipped through. Lake TOML decoding and Lean syntax manipulation utilities have also undergone significant rework to facilitate this PR. Such utilities are considered internal and thus little has been done to mitigate possible downstream breakages. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases | ||
| 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
- 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).