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> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| CMakeLists.txt | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||