From 2aeeed13cf3dcfb71ae4ceca801956a8540195f7 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 9 Aug 2023 11:54:53 -0400 Subject: [PATCH] fix: generalize Prod.lexAccessible to match Lean 3 (#2388) * fix: generalize Prod.lexAccessible to match Lean 3 * fix * fix --- src/Init/WF.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/WF.lean b/src/Init/WF.lean index f005f78f96..472489ff1f 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -222,8 +222,8 @@ section variable {α : Type u} {β : Type v} variable {ra : α → α → Prop} {rb : β → β → Prop} -def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by - induction (aca a) generalizing b with +def lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by + induction aca generalizing b with | intro xa _ iha => induction (acb b) with | intro xb _ ihb => @@ -236,7 +236,7 @@ def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a -- The lexicographical order of well founded relations is well-founded @[reducible] def lex (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where rel := Prod.Lex ha.rel hb.rel - wf := ⟨fun (a, b) => lexAccessible (WellFounded.apply ha.wf) (WellFounded.apply hb.wf) a b⟩ + wf := ⟨fun (a, b) => lexAccessible (WellFounded.apply ha.wf a) (WellFounded.apply hb.wf) b⟩ instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β) := lex ha hb