Documentation

Mathlib.Lean.Json

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

source
@[implicit_reducible]
instance Lean.instFromJsonPUnit_mathlib :
FromJson PUnit
source
def Lean.instFromJsonPUnit_mathlib.fromJson :
Json → Except String PUnit
Instances For
    source
    @[implicit_reducible]
    instance Lean.instToJsonPUnit_mathlib :
    ToJson PUnit
    source
    def Lean.instToJsonPUnit_mathlib.toJson :
    PUnit → Json
    Instances For
      source
      @[implicit_reducible]
      instance Lean.instFromJsonFin_mathlib {n : Nat} :
      FromJson (Fin n)
      source
      @[implicit_reducible]
      instance Lean.instToJsonFin_mathlib {n : Nat} :
      ToJson (Fin n)
      source
      @[implicit_reducible]
      instance Lean.instFromJsonSubtypeOfDecidablePred_mathlib {α : Type u} [FromJson α] (p : α → Prop) [DecidablePred p] :
      FromJson (Subtype p)
      source
      @[implicit_reducible]
      instance Lean.instToJsonSubtype_mathlib {α : Type u} [ToJson α] (p : α → Prop) :
      ToJson (Subtype p)