fix: use _mustInline in lambdas only

2022-08-21 16:41:18 -07:00 · 2022-08-21 16:41:18 -07:00 · bc5b6272d8
commit bc5b6272d8
parent d11947abc0
1 changed files with 1 additions and 1 deletions
--- 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