Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
1f9bba9d39
This PR refactors the Lake codebase to use the new module system throughout. Every module in `Lake` is now a `module`. As this was already a large-scale refactor, a general cleanup of the code has also been bundled in. This PR also uses workarounds for currently outstanding module system issues: #10061, #10062, #10063, #10064, #10065, #10067, and #10068. **Breaking change:** Since the module system encourages a `private`-by-default design, the Lake API has switched from its previous `public`-by-default approach. As such, many definitions that were previously public are now private. The newly private definitions are not expected to have had significant user use, Nonetheless, important use cases could be missed. If a key API is now inaccessible but seems like it should be public, users are encouraged to report this as an issue on GitHub. |
||
|---|---|---|
| .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 Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.