8f508e3c91
This PR closes https://github.com/leanprover/lean4/issues/13770 by including `Config.zetaUnused` in `Config.toKey`. Without this, two configs that differ only in `zetaUnused` share a `WHNF`/`isDefEq` cache key, so reductions performed under one setting can be returned for the other. The new bit sits at position 22, immediately above `zetaHave`. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
16 lines
433 B
Text
16 lines
433 B
Text
module
|
|
|
|
import Lean
|
|
|
|
/-!
|
|
Regression test for https://github.com/leanprover/lean4/issues/13770.
|
|
|
|
`Meta.Config.zetaUnused` controls `whnfCore`/`isDefEqQuick` reduction of unused `let`/`have`
|
|
bindings, so two configs differing only in `zetaUnused` must produce distinct cache keys.
|
|
-/
|
|
|
|
open Lean Meta
|
|
|
|
#guard
|
|
({ zetaUnused := false } : Meta.Config).toConfigWithKey.key !=
|
|
({ zetaUnused := true } : Meta.Config).toConfigWithKey.key
|