mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
24380fc900
This PR enables the `cbv` tactic to unfold nullary (non-function) constant definitions such as `def myNat : Nat := 42`, allowing ground term evaluation (e.g. `evalEq`, `evalLT`) to recognize their values as literals. Previously, `handleConst` skipped all nullary constants. Now it performs direct delta reduction using `instantiateValueLevelParams` instead of going through the equation theorem machinery (`getUnfoldTheorem`), which would trigger `realizeConst` and fail for constants (such as derived typeclass instances) where `enableRealizationsForConst` has not been called. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
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.