Documentation

Lean.Compiler.IR.Format

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