diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index b62d3b274d..f2bf9e24f1 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -303,6 +303,7 @@ def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do unless (← shouldInlineLocal decl) do return none let numArgs := e.getAppNumArgs let arity := decl.getArity + -- TODO: we should inline/specialize partial applications of local functions if numArgs < arity then return none incInlineLocal modify fun s => { s with inlineLocal := s.inlineLocal + 1 }