Documentation

Lean.Data.Json.Printer

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

Equations

Lean.Json.escape s = String.foldl Lean.Json.escapeAux "" s

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

Equations

Lean.Json.renderString s = "\"" ++ Lean.Json.escape s ++ "\""

partial def Lean.Json.render :

Lean.Json → Lean.Format

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

Equations

Lean.Json.pretty j lineWidth = Lean.Format.pretty (Lean.Json.render j) lineWidth

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) :

Equations

Lean.Json.compress j = (fun go => go "" [Lean.Json.CompressWorkItem.json j]) Lean.Json.compress.go

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

List Lean.Json.CompressWorkItem → String

instance Lean.Json.instToFormatJson :

Lean.ToFormat Lean.Json

Equations

Lean.Json.instToFormatJson = { format := Lean.Json.render }

instance Lean.Json.instToStringJson :

ToString Lean.Json

Equations

Lean.Json.instToStringJson = { toString := fun j => Lean.Json.pretty j }