From c769808a4e33e4e2af97afa6df3ec7d9eb9c5505 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Sep 2022 19:35:17 -0700
Subject: [PATCH] chore: add TODO

---
 src/Lean/Compiler/LCNF/Simp.lean | 1 +
 1 file changed, 1 insertion(+)

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 }