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

Equations

• Lean.Compiler.LCNF.isCompilerRelevantMData _mdata = false

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

Return true if e is a lcCast application.

Equations

• Lean.Compiler.LCNF.isLcCast? e = if Lean.Expr.isAppOfArity e (Lean.Name.mkStr1 "lcCast") 3 = true then some (Lean.Expr.appArg! e) else none

structure Lean.Compiler.LCNF.CasesInfo : Type

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

Store information about casesOn declarations.

We treat them uniformly in the code generator.

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

Equations

• Lean.Compiler.LCNF.CasesInfo.numAlts c = Array.size c.altNumParams

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

Equations

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

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

Equations

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

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

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

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.

Equations

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