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

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

Return true if e is a lcCast application.

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

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

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

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

def Lean.Compiler.LCNF.builtinRuntimeTypes : Array Name

List of types that have builtin runtime support

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

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