Equations
Instances For
Equations
- Lean.Json.renderString s = "\"" ++ Lean.Json.escape s ++ "\""
Instances For
- 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
Instances For
Equations
- j.compress = Lean.Json.compress.go "" [Lean.Json.CompressWorkItem.json j]
Instances For
Equations
- Lean.Json.instToFormat = { format := Lean.Json.render }
Equations
- Lean.Json.instToString = { toString := fun (j : Lean.Json) => j.pretty }