- 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