diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index cbe260ec75..f28c5e7d32 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -156,9 +156,6 @@ partial def inlineApp? (letDecl : LetDecl) (k : Code) : SimpM (Option Code) := d code.bind fun fvarId' => do markUsedFVar fvarId' simpK fvarId' - -- else if info.ifReduce then - -- eraseCode code - -- return none else markSimplified let expectedType ← inferAppType info.fType info.args[*...info.arity]