Json serialization typeclass for PUnit & Fin n & Subtype p

instance Lean.instFromJsonPUnit_mathlib : FromJson PUnit

Equations

• Lean.instFromJsonPUnit_mathlib = { fromJson? := Lean.fromJsonPUnit✝ }

instance Lean.instToJsonPUnit_mathlib : ToJson PUnit

Equations

• Lean.instToJsonPUnit_mathlib = { toJson := Lean.toJsonPUnit✝ }

instance Lean.instFromJsonFin_mathlib {n : Nat} : FromJson (Fin n)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToJsonFin_mathlib {n : Nat} : ToJson (Fin n)

Equations

• Lean.instToJsonFin_mathlib = { toJson := fun (i : Fin n) => Lean.toJson ↑i }

instance Lean.instFromJsonSubtypeOfDecidablePred_mathlib {α : Type u} [FromJson α] (p : α → Prop) [DecidablePred p] : FromJson (Subtype p)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToJsonSubtype_mathlib {α : Type u} [ToJson α] (p : α → Prop) : ToJson (Subtype p)

Equations

• Lean.instToJsonSubtype_mathlib p = { toJson := fun (x : Subtype p) => Lean.toJson x.val }