def Lean.Compiler.LCNF.isCompilerRelevantMData (_mdata : MData) : Bool

Return true if mdata should be preserved. Right now, we don't preserve any MData, but this may change in the future when we add support for debugging information

Equations

• Lean.Compiler.LCNF.isCompilerRelevantMData _mdata = false

def Lean.Compiler.LCNF.isLcCast? (e : Expr) : Option Expr

Return true if e is a lcCast application.

Equations

• Lean.Compiler.LCNF.isLcCast? e = if e.isAppOfArity `lcCast 3 = true then some e.appArg! else none

def Lean.Compiler.LCNF.getCtorArity? (declName : Name) : CoreM (Option Nat)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.builtinRuntimeTypes : Array Name

List of types that have builtin runtime support

Equations

• Lean.Compiler.LCNF.builtinRuntimeTypes = #[`String, `UInt8, `UInt16, `UInt32, `UInt64, `USize, `Float, `Float32, `Thunk, `Task, `Array, `ByteArray, `FloatArray, `Nat, `Int]

def Lean.Compiler.LCNF.isRuntimeBuiltinType (declName : Name) : Bool

Return true iff declName is the name of a type with builtin support in the runtime.

Equations

• Lean.Compiler.LCNF.isRuntimeBuiltinType declName = Lean.Compiler.LCNF.builtinRuntimeTypes.contains declName