Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
2f8c85af89
This PR fixes #12495 where equational theorem generation fails for structurally recursive definitions using a Box-like wrapper around nested inductives. ## Root Cause `withInferTypeConfig` (in `InferType.lean`) ensures various MetaM config settings (`beta`, `iota`, `zeta`, `zetaHave`, `zetaDelta`, `proj`) are enabled during type inference, but was missing `etaStruct`. When `inferType` is called from a context where `etaStruct` is disabled — such as inside `simpMatch` (which sets `etaStruct := .none` via `SimpM.run` → `withSimpContext`) — `whnf` cannot eta-expand structure values needed for recursor iota reduction. Concretely, projecting from a type like `Rec.rec_2 ... base` (where `base : Box Rec`) requires eta-expanding `base` to `Box.mk base.data` so the `Box` recursor can reduce. With `etaStruct := .none`, `toCtorWhenStructure` skips the eta-expansion, leaving `whnf` stuck and `inferProjType` unable to recognize the resulting type as a structure. ## Fix Add `etaStruct := .all` to the config settings ensured by `withInferTypeConfig`, alongside the existing `beta`, `iota`, `zeta`, `zetaHave`, `zetaDelta`, and `proj` settings. This also allows reverting the workaround (`try/catch` around `simpMatch?`) that was added in the first commit. ## Test plan - [x] Existing test `tests/lean/run/issue12495.lean` passes - [x] Full test suite (3561 tests) passes with 0 failures 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .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.