096e4eb6d0
The issue was raised on Zulip. The issue is triggered in declarations containing overlapping patterns and nested recursive definitions occurring as the discriminant of `match`-expressions. Recall that Lean 4 generates conditional equations for declarations containing overlapping patterns. To address the issue we had to "fold" `WellFounded.fix` applications back as recursive applications of the functions being defined. The new test exposes the issue. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||