Documentation

Lean.Compiler.LCNF.Util

source
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
source
def Lean.Compiler.LCNF.isLcCast? (e : Lean.Expr) :
Option Lean.Expr

Return true if e is a lcCast application.

Equations
source
structure Lean.Compiler.LCNF.CasesInfo :
Type

Store information about casesOn declarations.

We treat them uniformly in the code generator.

Instances For
    source
    def Lean.Compiler.LCNF.CasesInfo.numAlts (c : Lean.Compiler.LCNF.CasesInfo) :
    Nat
    Equations
    source
    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.
    source
    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.
    source
    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.
    source
    def Lean.Compiler.LCNF.builtinRuntimeTypes :
    List Lean.Name

    List of types that have builtin runtime support

    Equations
    source
    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