diff --git a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean index aa2fa43189..d533eea51e 100644 --- a/src/Lean/Compiler/LCNF/Simp/SimpValue.lean +++ b/src/Lean/Compiler/LCNF/Simp/SimpValue.lean @@ -32,6 +32,7 @@ def simpAppApp? (e : Expr) : OptionT SimpM Expr := do guard f.isFVar let f ← findExpr f guard <| f.isApp || f.isConst + guard <| !f.isAppOf ``lcCast markSimplified return mkAppN f e.getAppArgs