Skip to content

Commit 5778a3c

Browse files
authored
chore: fix "isRuntimeBultinType" typo (#9307)
1 parent 668a892 commit 5778a3c

File tree

3 files changed

+3
-3
lines changed

3 files changed

+3
-3
lines changed

src/Lean/Compiler/LCNF/MonoTypes.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
5252
trivialStructureInfoExt.insert declName info?
5353
return info?
5454
where fillCache : CoreM (Option TrivialStructureInfo) := do
55-
if isRuntimeBultinType declName then return none
55+
if isRuntimeBuiltinType declName then return none
5656
let .inductInfo info ← getConstInfo declName | return none
5757
if info.isUnsafe || info.isRec then return none
5858
let [ctorName] := info.ctors | return none

src/Lean/Compiler/LCNF/ToLCNF.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -671,7 +671,7 @@ where
671671

672672
visitProjFn (projInfo : ProjectionFunctionInfo) (e : Expr) : M Arg := do
673673
let typeName := projInfo.ctorName.getPrefix
674-
if isRuntimeBultinType typeName then
674+
if isRuntimeBuiltinType typeName then
675675
let numArgs := e.getAppNumArgs
676676
let arity := projInfo.numParams + 1
677677
if numArgs < arity then

src/Lean/Compiler/LCNF/Util.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ def builtinRuntimeTypes : Array Name := #[
8989
/--
9090
Return `true` iff `declName` is the name of a type with builtin support in the runtime.
9191
-/
92-
def isRuntimeBultinType (declName : Name) : Bool :=
92+
def isRuntimeBuiltinType (declName : Name) : Bool :=
9393
builtinRuntimeTypes.contains declName
9494

9595
end Lean.Compiler.LCNF

0 commit comments

Comments
 (0)