Documentation

Init.Data.ToString.Basic

class ToString (α : Type u) :
Instances
    Equations
    Equations
    Equations
    def List.toString {α : Type u_1} [ToString α] :
    List αString
    Equations
    Instances For
      instance instToStringList {α : Type u} [ToString α] :
      Equations
      Equations
      instance instToStringULift {α : Type u} [ToString α] :
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      instance instToStringFin (n : Nat) :
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      instance instToStringOption {α : Type u} [ToString α] :
      Equations
      instance instToStringSum {α : Type u} {β : Type v} [ToString α] [ToString β] :
      Equations
      • One or more equations did not get rendered due to their size.
      instance instToStringProd {α : Type u} {β : Type v} [ToString α] [ToString β] :
      Equations
      instance instToStringSigma {α : Type u} {β : αType v} [ToString α] [(x : α) → ToString (β x)] :
      Equations
      instance instToStringSubtype {α : Type u} {p : αProp} [ToString α] :
      Equations
      Equations
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            instance instToStringExcept {ε : Type u_1} {α : Type u_2} [ToString ε] [ToString α] :
            Equations
            instance instReprExcept {ε : Type u_1} {α : Type u_2} [Repr ε] [Repr α] :
            Repr (Except ε α)
            Equations
            • One or more equations did not get rendered due to their size.