From e30303e33c92cc66211f382bd10be4ba7679b033 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Thu, 29 May 2025 14:11:21 -0700
Subject: [PATCH] fix: extract more Nats in extractClosed (#8535)

This PR extracts more Nats (and their downstream users) in extractClosed
by fixing a silly oversight in the logic.
---
 src/Lean/Compiler/LCNF/ExtractClosed.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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