We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0877819 commit cbbeaeeCopy full SHA for cbbeaee
src/Lean/Compiler/LCNF/ExtractClosed.lean
@@ -76,6 +76,7 @@ mutual
76
partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
77
match v with
78
| .lit (.str _) => return true
79
+ | .lit (.nat v) => return !isRoot || v >= Nat.pow 2 63
80
| .lit _ | .erased => return !isRoot
81
| .const name _ args =>
82
if (← read).sccDecls.any (·.name == name) then
0 commit comments