Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
7a7440f59b
Currently, `ll_infer_type` is responsible for telling the user about `noncomputable` when a definition depends on one without executable code. However, this is imperfect because type inference does not check every subexpression. This leads to errors later on that users find to be hard to interpret. Now, `Lean.IR.checkDecls` has a friendlier error message when it encounters constants without compiled definitions, suggesting to consider using `noncomputable`. While this function is an internal IR consistency check, it is also reasonable to have it give an informative error message in this particular case. The suggestion to use `noncomputable` is limited to just unknown constants. Some alternatives would be to either (1) create another checker just for missing constants, (2) change `ll_infer_type` to always visit every subexpression no matter if they are necessary for inferring the type, or (3) investigate whether `tests/lean/run/1785.lean` is due to a deeper issue. Closes #1785 |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| debug.log | ||
| 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).