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

structure Lean.Compiler.LCNF.CasesInfo : Type

Store information about casesOn declarations.

We treat them uniformly in the code generator.

• declName : Name
• arity : Nat
• numParams : Nat
• discrPos : Nat
• altsRange : Std.Range
• altNumParams : Array Nat
• motivePos : Nat

def Lean.Compiler.LCNF.CasesInfo.numAlts (c : CasesInfo) : Nat

Equations

• c.numAlts = c.altNumParams.size

def Lean.Compiler.LCNF.getCasesInfo? (declName : Name) : CoreM (Option CasesInfo)

Equations

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

def Lean.Compiler.LCNF.isCasesApp? (e : Expr) : CoreM (Option CasesInfo)

Equations

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

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.isRuntimeBultinType (declName : Name) : Bool

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

Equations

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