Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
48491e5262
This PR changes elaboration of `structure` parents so that each must be fully elaborated before the next one is processed. In particular, it re-adds synthesizing synthetic mvars between `structure` parents, in the same manner as other fields. This synthesis step was removed in #5842 because I had thought parents were like type parameters and would participate in header elaboration, but in the end it made more sense elaborating parents after the headers are done, since they're like fields. We want this enabled because it will help ensure that all the necessary reductions are done to types of fields as they're added to the structure. |
||
|---|---|---|
| .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).