max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: make builtinRuntimeTypes an Array rather than a List (#8249)

Browse source
This commit is contained in:
Cameron Zwarich 2025-05-06 09:27:05 -07:00 • committed by GitHub
parent c96dfa54a4
commit cd100b8832
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/LCNF/Util.lean
View file

@ -77,7 +77,7 @@ def getCtorArity? (declName : Name) : CoreM (Option Nat) := do
/--
List of types that have builtin runtime support
-/
def builtinRuntimeTypes : List Name := [
def builtinRuntimeTypes : Array Name := #[
``String,
``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize,
``Float, ``Float32,