instance
Lean.instFromJsonSubtype
{α : Type u}
[Lean.FromJson α]
(p : α → Prop)
[DecidablePred p]
:
Lean.FromJson (Subtype p)
instance
Lean.instToJsonSubtype
{α : Type u}
[Lean.ToJson α]
(p : α → Prop)
:
Lean.ToJson (Subtype p)
Mathlib.Lean.Json