mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
95583d74bd
This PR fixes an inconsistency in `getStuckMVar?` where the instance argument to class projection functions and auxiliary parent projections was not whnf-normalized before checking for stuck metavariables. Every other case in `getStuckMVar?` (recursors, quotient recursors, `.proj` nodes) normalizes the major argument via `whnf` before recursing — class projection functions and aux parent projections were the exception. This bug was identified by Matthew Jasper. When the instance parameter to a class projection is not normalized, `getStuckMVar?` may fail to detect stuck metavariables that would be revealed by whnf, or conversely may report stuckness for expressions that would reduce to constructors. This caused issues with `OfNat` and `Zero` at `with_reducible_and_instances` transparency. Note: PR #12701 (already merged) is also required to fix the original Mathlib examples.
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.