Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
f15d531acb
This PR replaces some `HashSet Expr`-typed collections of facts in `omega`'s implementation with plain lists. This change makes some `omega` calls faster, some slower, but the advantage is that `omega`'s performance is more independent the state of the name generator that produces fvar IDs. I've created this PR for discussion and am happy to hear opinions on whether this should be merged or not. A good reason *not* to merge is that it causes regressions in some places and `grind` is expected to supersede `omega` either way. A good reason to merge is that `omega` is used all over the place and its flaky performance increases the noise in future benchmarks. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| 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.