Json serialization typeclass for PUnit & Fin n & Subtype p

instance Lean.instFromJsonPUnit_mathlib : Lean.FromJson PUnit

Equations

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

instance Lean.instToJsonPUnit_mathlib : Lean.ToJson PUnit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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