Documentation

Lean.Compiler.LCNF.Util

source
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

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

    Return true if e is a lcCast application.

    Instances For
      source
      def Lean.Compiler.LCNF.getCtorArity? (declName : Name) :
      CoreM (Option Nat)
      Instances For
        source
        def Lean.Compiler.LCNF.builtinRuntimeTypes :
        Array Name

        List of types that have builtin runtime support

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

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

          Instances For