Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
fb1dc9112b
This PR changes the behavior of forward and backward projection propagation in the context of user defined borrows. The reason to have them be "forced" override (i.e. override user annotations as well) was that a user annotated borrowed value can potentially flow into a reset-reuse transitively through a projection and must thus have accurate reference count. The reasons that this is no longer necessary are: 1. Forward never had to be forced anyways, it can only affect the `z` in `let z := oproj x i` which can't be annotated by a user 2. Backward is no longer necessary as the forward propagator for user annotations prevents the reset-reuse insertion from working with values that have user defined borrow annotations entirely. |
||
|---|---|---|
| .claude | ||
| .github | ||
| .vscode | ||
| 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 | ||
| 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.