Documentation

Lean.Data.Json.Printer

source
@[inline]
def Lean.Json.escape (s : String) (acc : String := "") :
String
Equations
    Instances For
      source
      @[inline]
      def Lean.Json.renderString (s : String) (acc : String := "") :
      String
      Equations
        Instances For
          source
          partial def Lean.Json.render :
          Json → Format
          source
          def Lean.Json.pretty (j : Json) (lineWidth : Nat := 80) :
          String
          Equations
            Instances For
              source
              def Lean.Json.compress (j : Json) :
              String
              Equations
                Instances For
                  source
                  instance Lean.Json.instToFormat :
                  ToFormat Json
                  Equations
                    source
                    instance Lean.Json.instToString :
                    ToString Json
                    Equations