Documentation

Lean.Compiler.IR.Format

source
instance Lean.IR.instToFormatArg :
Lean.ToFormat Lean.IR.Arg
source
def Lean.IR.formatArray {α : Type} [Lean.ToFormat α] (args : Array α) :
Lean.Format
Instances For
    source
    instance Lean.IR.instToFormatLitVal :
    Lean.ToFormat Lean.IR.LitVal
    source
    instance Lean.IR.instToFormatCtorInfo :
    Lean.ToFormat Lean.IR.CtorInfo
    source
    instance Lean.IR.instToFormatExpr :
    Lean.ToFormat Lean.IR.Expr
    source
    instance Lean.IR.instToStringExpr :
    ToString Lean.IR.Expr
    source
    instance Lean.IR.instToFormatIRType :
    Lean.ToFormat Lean.IR.IRType
    source
    instance Lean.IR.instToStringIRType :
    ToString Lean.IR.IRType
    source
    instance Lean.IR.instToFormatParam :
    Lean.ToFormat Lean.IR.Param
    source
    def Lean.IR.formatAlt (fmt : Lean.IR.FnBody → Lean.Format) (indent : Nat) :
    Lean.IR.Alt → Lean.Format
    Instances For
      source
      def Lean.IR.formatParams (ps : Array Lean.IR.Param) :
      Lean.Format
      Instances For
        source
        def Lean.IR.formatFnBodyHead :
        Lean.IR.FnBody → Lean.Format
        Instances For
          source
          def Lean.IR.formatFnBody (fnBody : Lean.IR.FnBody) (indent : optParam Nat 2) :
          Lean.Format
          Instances For
            source
            partial def Lean.IR.formatFnBody.loop (indent : optParam Nat 2) :
            Lean.IR.FnBody → Lean.Format
            source
            instance Lean.IR.instToFormatFnBody :
            Lean.ToFormat Lean.IR.FnBody
            source
            instance Lean.IR.instToStringFnBody :
            ToString Lean.IR.FnBody
            source
            def Lean.IR.formatDecl (decl : Lean.IR.Decl) (indent : optParam Nat 2) :
            Lean.Format
            Instances For
              source
              instance Lean.IR.instToFormatDecl :
              Lean.ToFormat Lean.IR.Decl
              source
              @[export lean_ir_decl_to_string]
              def Lean.IR.declToString (d : Lean.IR.Decl) :
              String
              Instances For
                source
                instance Lean.IR.instToStringDecl :
                ToString Lean.IR.Decl