Json serialization typeclass for PUnit & Fin n & Subtype p

instance Lean.instFromJsonPUnit : Lean.FromJson PUnit

Equations

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

instance Lean.instToJsonPUnit : Lean.ToJson PUnit

Equations

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

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

Equations

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

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

Equations

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

instance Lean.instFromJsonSubtype {α : 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 {α : Type u} [Lean.ToJson α] (p : α → Prop) : Lean.ToJson (Subtype p)

Equations

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