Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
e0c1afd12d
Closes #3386 Currently, when generating the signature of an injectivity lemma for a certain constructor `c : forall xs, Foo a_1 ... a_n`, `mkInjectiveTheoremTypeCore?` will differentiate between variables which are bound to stay the same between the two equal values (i.e inductive indices), and non-fixed ones. To do that, the function currently checks whether a variable `x ∈ xs` appears in the final co-domain `Foo a_1 ... a_n` of the constructor. This condition isn't enough however. As shown in the linked issue, the codomain may also depend on variables which appears in the type of free vars contained in `Foo a_1 ... a_n`, but not in the term itself. This PR fixes the issue by also checking the types of any free variable occuring in the final codomain, so as to ensure injectivity lemmas are well-typed. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| 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
- Manual
- 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).