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. |
||
|---|---|---|
| .. | ||
| Structural | ||
| WF | ||
| Basic.lean | ||
| Eqns.lean | ||
| Main.lean | ||
| MkInhabitant.lean | ||
| Structural.lean | ||
| WF.lean | ||