Documentation

Mathlib.Lean.Json

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

source
instance Lean.instFromJsonPUnit_mathlib :
FromJson PUnit
Equations
    source
    def Lean.instFromJsonPUnit_mathlib.fromJson :
    Json → Except String PUnit
    Equations
      Instances For
        source
        instance Lean.instToJsonPUnit_mathlib :
        ToJson PUnit
        Equations
          source
          def Lean.instToJsonPUnit_mathlib.toJson :
          PUnit → Json
          Equations
            Instances For
              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