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

chore: remove unnecessary eqvTypes

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-13 06:08:51 -07:00
parent aae12d5ee2
commit c33b5b6588
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Compiler/LCNF/Simp/Main.lean
View file

@ -96,10 +96,8 @@ def isReturnOf (c : Code) (fvarId : FVarId) : SimpM Bool := do
| .return fvarId' => return (← normFVar fvarId') == fvarId
| _ => return false
def elimVar? (value : Expr) (expectedType : Expr) : SimpM (Option FVarId) := do
def elimVar? (value : Expr) : SimpM (Option FVarId) := do
let .fvar fvarId := value | return none
let type ← getType fvarId
unless type.isErased || eqvTypes type expectedType do return none
return fvarId
mutual
@ -225,7 +223,7 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
attachCodeDecls decls k
else if let some funDecl ← etaPolyApp? decl then
simp (.fun funDecl k)
else if let some fvarId ← elimVar? decl.value decl.type then
else if let some fvarId ← elimVar? decl.value then
/- Eliminate `let _x_i := _x_j;` -/
addFVarSubst decl.fvarId fvarId
eraseLetDecl decl