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

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

    Return true if e is a lcCast application.

    Instances For
      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
        Instances For
          source
          def Lean.Compiler.LCNF.getCasesInfo? (declName : Lake.Name) :
          Lean.CoreM (Option Lean.Compiler.LCNF.CasesInfo)
          Instances For
            source
            def Lean.Compiler.LCNF.isCasesApp? (e : Lean.Expr) :
            Lean.CoreM (Option Lean.Compiler.LCNF.CasesInfo)
            Instances For
              source
              def Lean.Compiler.LCNF.getCtorArity? (declName : Lake.Name) :
              Lean.CoreM (Option Nat)
              Instances For
                source
                def Lean.Compiler.LCNF.builtinRuntimeTypes :
                List Lake.Name

                List of types that have builtin runtime support

                Instances For
                  source
                  def Lean.Compiler.LCNF.isRuntimeBultinType (declName : Lake.Name) :
                  Bool

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

                  Instances For