Documentation

Mathlib.Lean.Json

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

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Lean.instToJsonFin_mathlib = { toJson := fun (i : Fin n) => Lean.toJson i }
Equations
  • One or more equations did not get rendered due to their size.
instance Lean.instToJsonSubtype_mathlib {α : Type u} [Lean.ToJson α] (p : αProp) :
Equations