def Lean.Json.escape (s : String) (acc : String := "") : String

def Lean.Json.renderString (s : String) (acc : String := "") : String

partial def Lean.Json.render : Json → Format

def Lean.Json.pretty (j : Json) (lineWidth : Nat := 80) : String

inductive Lean.Json.CompressWorkItem : Type

• json (j : Json) : Json.CompressWorkItem
• arrayElem (j : Json) : Json.CompressWorkItem
• arrayEnd : Json.CompressWorkItem
• objectField (k : String) (j : Json) : Json.CompressWorkItem
• objectEnd : Json.CompressWorkItem
• comma : Json.CompressWorkItem

def Lean.Json.compress (j : Json) : String

partial def Lean.Json.compress.go (acc : String) : List Json.CompressWorkItem → String

instance Lean.Json.instToFormat : ToFormat Json

instance Lean.Json.instToString : ToString Json