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

chore(library/init/core): make sure new frontend can parse it

Browse source 
@kha This is a temporary fix. We will get back to the new frontend after
we submit the IR paper.
This commit is contained in:
Leonardo de Moura 2019-05-03 17:36:39 -07:00
parent 86faa5ade4
commit 82d88dc96f
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/core.lean
View file

@ -1278,9 +1278,9 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
{decEq := λ ⟨a, b⟩ ⟨a', b'⟩,
match (decEq a a') with
| (isTrue e₁) :=
match (decEq b b') with
| (isTrue e₂) := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
| (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂))
(match (decEq b b') with
| (isTrue e₂) := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
| (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
| (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
instance [HasLess α] [HasLess β] : HasLess (α × β) :=