diff --git a/src/Init/WF.lean b/src/Init/WF.lean index d73bdcff50ff..4ad3a6f1707a 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -173,7 +173,7 @@ namespace Nat -- less-than is well-founded def lt_wfRel : WellFoundedRelation Nat where - rel := Nat.lt + rel := (· < ·) wf := by apply WellFounded.intro intro n