Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
fedf235cba
In Lean 4, we have support for typing constraints of the form ``` (?m ...).1 =?= v ``` where the type of `?m ...` is a structure with a single field. This kind of constraint is reduced to `?m ... =?= ⟨v⟩` This feature is implemented by the function `isDefEqSingleton`. As far as I remember, Lean 3 does not implement this feature. This commit disables this feature if the structure is a class. The goal is to avoid the generation of counterintuitive instances by typing inference. For example, in the example at issue #2011, the following weird instance was being generated for `Zero (f x)` ``` (@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝) ``` where `inst✝¹` is the local instance `[∀ i, Zero (f i)]` Note that this instance is definitinally equal to the expected nicer instance `inst✝¹ x✝`. However, the nasty instance trigger nasty unification higher order constraints later. Note that a few tests broke because different error messages were produced. The new error messages seem better. I do not expect this change to affect Mathlib4 since Lean 3 does not have this feature. |
||
|---|---|---|
| .github | ||
| .vscode | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitmodules | ||
| .ignore | ||
| CMakeLists.txt | ||
| CONTRIBUTING.md | ||
| default.nix | ||
| flake.lock | ||
| flake.nix | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
| shell.nix | ||
This is the repository for Lean 4, which is currently being released as milestone releases towards a first stable release. Lean 3 is still the latest stable release.
About
- Quickstart
- Walkthrough installation video
- Quick tour video
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean first chapter is available!
- Manual
- Release notes starting at v4.0.0-m3
- Examples
- FAQ
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.