def Lean.Compiler.LCNF.isCompilerRelevantMData (_mdata : Lean.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 : Lean.Expr) : Option Lean.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 : Lean.Name
• arity : Nat
• numParams : Nat
• discrPos : Nat
• altsRange : Std.Range
• altNumParams : Array Nat
• motivePos : Nat

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

Equations

• c.numAlts = c.altNumParams.size

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

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

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

Equations

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

def Lean.Compiler.LCNF.builtinRuntimeTypes : List Lean.Name

List of types that have builtin runtime support

Equations

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

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

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