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}
Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance Lean.instFromJsonPUnit_mathlib :
    FromJson PUnit.{u_1 + 1}
    source
    🔸 coverage
    @[implicit_reducible]
    instance Lean.instToJsonPUnit_mathlib :
    ToJson PUnit.{u_1 + 1}
    source
    🔸 coverage
    def Lean.instToJsonPUnit_mathlib.toJson :
    PUnit.{u_1} → Json
    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance Lean.instFromJsonFin_mathlib {n : â„•} :
      FromJson (Fin n)
      source
      🔸 coverage
      @[implicit_reducible]
      instance Lean.instToJsonFin_mathlib {n : â„•} :
      ToJson (Fin n)
      source
      🔸 coverage
      @[implicit_reducible]
      instance Lean.instFromJsonSubtypeOfDecidablePred_mathlib {α : Type u} [FromJson α] (p : α → Prop) [DecidablePred p] :
      FromJson (Subtype p)
      source
      🔸 coverage
      @[implicit_reducible]
      instance Lean.instToJsonSubtype_mathlib {α : Type u} [ToJson α] (p : α → Prop) :
      ToJson (Subtype p)