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

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-15 06:26:04 -07:00
parent ef308e7f2c
commit bf7b105b74
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Deriving/DecEq.lean
View file

@ -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
)