2eca5ca6e4
This PR fixes a panic in `getEqnsFor?` when called on matchers generated from match expressions in theorem types. When a theorem's type contains a match expression (e.g., `theorem bar : (match ... with ...) = 0`), the compiler generates a matcher like `bar.match_1`. Calling `getEqnsFor?` on this matcher would panic with: ``` PANIC: duplicate normalized declaration name bar.match_1.eq_1 vs. _private...bar.match_1.eq_1 ``` This also affected the `try?` tactic, which internally uses `getEqnsFor?`. We make `shouldGenerateEqnThms` return `false` for matchers, since their equations are already generated separately by `Lean.Meta.Match.MatchEqs`. This prevents the equation generation machinery from attempting to create duplicate equation theorems. Closes #11461 Closes #10390 🤖 Prepared with Claude Code Co-authored-by: Claude <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||