From bf7b105b749e0106be01eda8c829a38914651cfa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Aug 2022 06:26:04 -0700 Subject: [PATCH] chore: remove workaround --- src/Lean/Elab/Deriving/DecEq.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index ee1ce78e9b..9e655ccddf 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -166,7 +166,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do fun x y => if h : x.toCtorIdx = y.toCtorIdx then -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct. - isTrue (by first | have aux : _ := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl) + isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl) else isFalse fun h => by subst h; contradiction )