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

fix: rewrite by with strict indentation in a few struct-fields

Browse source
This commit is contained in:
Adrien Champion 2022-11-08 13:13:37 +01:00 • committed by Leonardo de Moura
parent 1823735ebf
commit 33aa1724f2
1 changed files with 17 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/Init/WF.lean
View file

@ -151,20 +151,20 @@ namespace Nat
def lt_wfRel : WellFoundedRelation Nat where
rel := Nat.lt
wf := by
apply WellFounded.intro
intro n
induction n with
| zero =>
apply Acc.intro 0
intro _ h
apply absurd h (Nat.not_lt_zero _)
| succ n ih =>
apply Acc.intro (Nat.succ n)
intro m h
have : m = n ∨ m < n := Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ h)
match this with
| Or.inl e => subst e; assumption
| Or.inr e => exact Acc.inv ih e
apply WellFounded.intro
intro n
induction n with
| zero =>
apply Acc.intro 0
intro _ h
apply absurd h (Nat.not_lt_zero _)
| succ n ih =>
apply Acc.intro (Nat.succ n)
intro m h
have : m = n ∨ m < n := Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ h)
match this with
| Or.inl e => subst e; assumption
| Or.inr e => exact Acc.inv ih e
protected theorem strongInductionOn
{motive : Nat → Sort u}
@ -256,9 +256,9 @@ def RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Lex ra rb
def rprod (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where
rel := RProd ha.rel hb.rel
wf := by
apply Subrelation.wf (r := Lex ha.rel hb.rel) (h₂ := (lex ha hb).wf)
intro a b h
exact RProdSubLex a b h
apply Subrelation.wf (r := Lex ha.rel hb.rel) (h₂ := (lex ha hb).wf)
intro a b h
exact RProdSubLex a b h
end