From 3331ed9bb1358a93fb75e3155aeb9ea12e89045c Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 30 Jan 2025 20:53:49 -0800 Subject: [PATCH] fix: add Float32 to LCNF.builtinRuntimeTypes list (#6837) This PR adds Float32 to the LCNF builtinRuntimeTypes list. This was missed during the initial Float32 implementation, but this omission has the side effect of lowering Float32 to obj in the IR. --- src/Lean/Compiler/LCNF/Util.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Util.lean b/src/Lean/Compiler/LCNF/Util.lean index e91a229f58..fac45e1764 100644 --- a/src/Lean/Compiler/LCNF/Util.lean +++ b/src/Lean/Compiler/LCNF/Util.lean @@ -80,7 +80,7 @@ List of types that have builtin runtime support def builtinRuntimeTypes : List Name := [ ``String, ``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize, - ``Float, + ``Float, ``Float32, ``Thunk, ``Task, ``Array, ``ByteArray, ``FloatArray, ``Nat, ``Int