Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
5db4f96699
This PR adds a module resolution procedure to Lake to disambiguate modules that are defined in multiple packages. On an `import`, Lake will now check if multiple packages within the workspace define the module. If so, it will verify that modules have sufficiently similar definitions (i.e., artifacts with the same content hashes). If not, Lake will report an error. This verification is currently only done for direct imports. Transitive imports are not checked for consistency. An overhaul of transitive imports will come later. |
||
|---|---|---|
| .claude | ||
| .github | ||
| doc | ||
| images | ||
| 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
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.