Documentation

Lean.Compiler.IR.Format

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