Documentation

Mathlib.Lean.Json

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

source
🔸 coverage
def Lean.instFromJsonPUnit_mathlib.fromJson :
Json → Except String PUnit.{u_1 + 1}
Equations
    Instances For
      source
      🔸 coverage
      instance Lean.instFromJsonPUnit_mathlib :
      FromJson PUnit.{u_1 + 1}
      Equations
        source
        🔸 coverage
        instance Lean.instToJsonPUnit_mathlib :
        ToJson PUnit.{u_1 + 1}
        Equations
          source
          🔸 coverage
          def Lean.instToJsonPUnit_mathlib.toJson :
          PUnit.{u_1} → Json
          Equations
            Instances For
              source
              🔸 coverage
              instance Lean.instFromJsonFin_mathlib {n : â„•} :
              FromJson (Fin n)
              Equations
                source
                🔸 coverage
                instance Lean.instToJsonFin_mathlib {n : â„•} :
                ToJson (Fin n)
                Equations
                  source
                  🔸 coverage
                  instance Lean.instFromJsonSubtypeOfDecidablePred_mathlib {α : Type u} [FromJson α] (p : α → Prop) [DecidablePred p] :
                  FromJson (Subtype p)
                  Equations
                    source
                    🔸 coverage
                    instance Lean.instToJsonSubtype_mathlib {α : Type u} [ToJson α] (p : α → Prop) :
                    ToJson (Subtype p)
                    Equations