From b305130ec3356b20000a6858a3bfe3797dad5d76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Fri, 13 Jan 2017 12:09:41 -0500 Subject: [PATCH] fix(library/init/wf): typo Same typo as #1091, different location. --- library/init/wf.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/wf.lean b/library/init/wf.lean index 13994eee69..547a202f10 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -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) :=