Equations
Instances For
- 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
Instances For
Instances For
Equations
- Lean.Json.instToFormat = { format := Lean.Json.render }
Equations
- Lean.Json.instToString = { toString := fun (j : Lean.Json) => j.pretty }