From 82d88dc96f9126941e42aa795c2e28a8c00bebca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 May 2019 17:36:39 -0700 Subject: [PATCH] chore(library/init/core): make sure new frontend can parse it @kha This is a temporary fix. We will get back to the new frontend after we submit the IR paper. --- library/init/core.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index c04946bdde..77a9a78345 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -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 (α × β) :=