def Lean.Json.escape (s : String) : String

def Lean.Json.renderString (s : String) : String

partial def Lean.Json.render : Lean.Json → Lean.Format

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

inductive Lean.Json.CompressWorkItem : Type

• json: Lean.Json → Lean.Json.CompressWorkItem
• arrayElem: Lean.Json → Lean.Json.CompressWorkItem
• arrayEnd: Lean.Json.CompressWorkItem
• objectField: String → Lean.Json → Lean.Json.CompressWorkItem
• objectEnd: Lean.Json.CompressWorkItem
• comma: Lean.Json.CompressWorkItem

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

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

instance Lean.Json.instToFormatJson : Lean.ToFormat Lean.Json

instance Lean.Json.instToStringJson : ToString Lean.Json