Documentation

Mathlib.Lean.Json

Json serialization typeclass for PUnit & Fin n & Subtype p #

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