87dae299b8
This PR ensures `ite` and `dite` are to selected as E-matching patterns. They are bad patterns because the then/else branches are only internalized after `grind` decided whether the condition is `True`/`False`. The issue reported by #9572 has been fixed, but the fix exposed another issue. The patterns for `List.Pairwise` produce an unbounded number of E-matching instances. ```lean example (l : List α) : l.Pairwise R := by grind ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||