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.

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

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