From fb6cb054655e85538d608bbc586c8d589050f2e7 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 12 Oct 2022 09:28:02 -0700
Subject: [PATCH] feat: support let_fun in new compiler

---
 src/Lean/Compiler/LCNF/ToLCNF.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index 035deeae17..08a489889e 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -714,7 +714,9 @@ where
       return .fvar funDecl.fvarId
 
   visitMData (mdata : MData) (e : Expr) : M Expr := do
-    if isCompilerRelevantMData mdata then
+    if let some (.app (.lam n t b ..) v) := letFunAnnotation? e then
+      visitLet (.letE n t v b (nonDep := true)) #[]
+    else if isCompilerRelevantMData mdata then
       mkAuxLetDecl <| .mdata mdata (← visit e)
     else
       visit e