max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: generalize Prod.lexAccessible to match Lean 3 (#2388)

Browse source 
* fix: generalize Prod.lexAccessible to match Lean 3

* fix

* fix
This commit is contained in:
Junyan Xu 2023-08-09 11:54:53 -04:00 • committed by GitHub
parent 8af25455ae
commit 2aeeed13cf
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/WF.lean
View file

@ -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