diff --git a/src/Lean/Compiler/LCNF/ExtractClosed.lean b/src/Lean/Compiler/LCNF/ExtractClosed.lean index 8c0679f623..d0aab0b289 100644 --- a/src/Lean/Compiler/LCNF/ExtractClosed.lean +++ b/src/Lean/Compiler/LCNF/ExtractClosed.lean @@ -63,7 +63,7 @@ partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do | .lit (.nat v) => -- The old compiler's implementation used the runtime's `is_scalar` function, which -- introduces a dependency on the architecture used by the compiler. - return v >= Nat.pow 2 63 + return !isRoot || v >= Nat.pow 2 63 | .lit _ | .erased => return !isRoot | .const name _ args => if (← read).sccDecls.any (·.name == name) then