From bc5b6272d8c99dcce16f9bc52696fdd689bb24c7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 21 Aug 2022 16:41:18 -0700
Subject: [PATCH] fix: use `_mustInline` in lambdas only

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

diff --git a/src/Lean/Compiler/Simp.lean b/src/Lean/Compiler/Simp.lean
index 1a5ee83c27..bb1e264a4b 100644
--- a/src/Lean/Compiler/Simp.lean
+++ b/src/Lean/Compiler/Simp.lean
@@ -177,7 +177,7 @@ where
     | .letE binderName type value body nonDep =>
       let idx ← modifyGet fun { nextIdx, localInfoMap } => (nextIdx, { nextIdx := nextIdx + 1, localInfoMap })
       let binderName' :=
-        if mustInline then
+        if mustInline && value.isLambda then
           .num `_mustInline idx
         else match binderName with
           | .num p _ => .num p idx