Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
3f4e85413e
This PR removes most cases where an error message explained that it was "probably due to metavariables," giving more explanation and a hint. ## Example ``` def square x := x * x ``` Before: ```lean4 typeclass instance problem is stuck, it is often due to metavariables HMul ?m.9 ?m.9 (?m.3 x) ``` After: ``` typeclass instance problem is stuck HMul ?m.9 ?m.9 (?m.3 x) Note: Lean will not try to resolve this typeclass instance problem because the first and second type arguments to `HMul` are metavariables. These arguments must be fully determined before Lean will try to resolve the typeclass. Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck. ``` In addition to providing beginner-and-intermediate-friendly explanation about **why** typeclass instance problems are treated as "stuck" when metavariables appear in output positions, this PR provides potentially-valuable improvement even to expert users: it explains **which of the typeclass arguments are inputs** and therefore need to be fully specified before typeclass resolution will be attempted. This information can be tricky to find otherwise. ## Next steps, but probably after this PR * error explanation * detecting when the syntactic source is a binop and giving a special-cased explanation on the binary operators and their associated typeclasses * detecting when the syntactic source is a function call, inspecting the function call's type somewhat, and replacing the generic "replace `x` with `(x : Nat)` hint with a specialized "replace `foo` with `foo (tyArg := Nat)`" hint |
||
|---|---|---|
| .claude | ||
| .github | ||
| 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 | ||
| 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
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.