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

Equations

• Lean.Json.escape s acc = String.foldl Lean.Json.escapeAux✝ acc s

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

Equations

• Lean.Json.renderString s acc = Lean.Json.escape s (acc ++ "\"") ++ "\""

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

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

Equations

• j.pretty lineWidth = j.render.pretty lineWidth

inductive Lean.Json.CompressWorkItem : Type

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

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

Equations

• j.compress = Lean.Json.compress.go "" [Lean.Json.CompressWorkItem.json j]

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

instance Lean.Json.instToFormat : Lean.ToFormat Lean.Json

Equations

• Lean.Json.instToFormat = { format := Lean.Json.render }

instance Lean.Json.instToString : ToString Lean.Json

Equations

• Lean.Json.instToString = { toString := fun (j : Lean.Json) => j.pretty }