From b60f97cc19464981f0ae194a944cbaf62ea358b1 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sat, 2 Aug 2025 08:18:41 -0700 Subject: [PATCH] chore: remove unused code in comment (#9687) --- src/Lean/Compiler/LCNF/Simp/Main.lean | 3 --- 1 file changed, 3 deletions(-) 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]