Documentation

Mathlib.Lean.Json

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

source
instance Lean.instFromJsonPUnit_mathlib :
FromJson PUnit
Equations
    source
    instance Lean.instToJsonPUnit_mathlib :
    ToJson PUnit
    Equations
      source
      instance Lean.instFromJsonFin_mathlib {n : Nat} :
      FromJson (Fin n)
      Equations
        source
        instance Lean.instToJsonFin_mathlib {n : Nat} :
        ToJson (Fin n)
        Equations
          source
          instance Lean.instFromJsonSubtypeOfDecidablePred_mathlib {α : Type u} [FromJson α] (p : α → Prop) [DecidablePred p] :
          FromJson (Subtype p)
          Equations
            source
            instance Lean.instToJsonSubtype_mathlib {α : Type u} [ToJson α] (p : α → Prop) :
            ToJson (Subtype p)
            Equations