instance Lean.instToJsonTreeMapStringCompare {α : Type u_1} [ToJson α] : ToJson (Std.TreeMap String α compare)

Equations

• Lean.instToJsonTreeMapStringCompare = { toJson := Lean.instToJsonTreeMapStringCompare._private_1 }

instance Lean.instFromJsonTreeMapString {α : Type} {cmp : String → String → Ordering} [FromJson α] : FromJson (Std.TreeMap String α cmp)

Equations

• Lean.instFromJsonTreeMapString = { fromJson? := Lean.instFromJsonTreeMapString._private_1 }