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

chore: remove unnecessary code

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-15 05:26:33 -07:00
parent aa68057c85
commit c3c0b8b8a2
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/PreDefinition/Eqns.lean
View file

@ -287,8 +287,9 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
let rec go (mvarId : MVarId) : MetaM Unit := do
if (← tryEqns mvarId) then
return ()
else if let some mvarId ← funext? mvarId then
go mvarId
-- Remark: we removed funext? from `mkEqnTypes`
-- else if let some mvarId ← funext? mvarId then
-- go mvarId
else if let some mvarId ← simpMatch? mvarId then
go mvarId
else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then