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

fix(library/init/wf): typo

Browse source 
Same typo as #1091, different location.
This commit is contained in:
François G. Dorais 2017-01-13 12:09:41 -05:00 • committed by Leonardo de Moura
parent 5f790d82cd
commit b305130ec3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/wf.lean
View file

@ -153,8 +153,8 @@ section
-- Lexicographical order based on ra and rb
inductive lex : α × β → α × β → Prop
| left : ∀ {a₁ b₁} a₂ b₂, ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
| right : ∀ a {b₁ b₂}, rb b₁ b₂ → lex (a, b₁) (a, b₂)
| left : ∀ {a₁} b₁ {a₂} b₂, ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
| right : ∀ a {b₁ b₂}, rb b₁ b₂ → lex (a, b₁) (a, b₂)
-- relational product based on ra and rb
inductive rprod : α × β → α × β → Prop
@ -183,7 +183,7 @@ section
-- relational product is a subrelation of the lex
def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b :=
λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb a₂ b₂ h₁)
λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb b₁ b₂ h₁)
-- The relational product of well founded relations is well-founded
def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) :=