cce6ce9577
This PR fixes #12245 where `grind` works on `Fin n` but fails on `Fin (n + 1)`. The `outParam` argument (e.g., the `range` parameter of `ToInt`) was included as a relevant position in the e-matching pattern. The `grind` normalizer rewrites `↑(n + 1)` to `↑n + 1` inside the range expression, causing the pattern to no longer match. Since `outParam` arguments are uniquely determined by type class resolution, they can be safely wildcarded in patterns — the same reasoning that already applies to instance-implicit arguments. Reproducer from the issue: ```lean example {n : Nat} {a : Fin (n + 1)} {b : Nat} (hb : b < n + 1) (h : (a : Nat) < b) : a < ⟨b, hb⟩ := by grind -- fails without fix ``` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- 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 | ||