Documentation

Init.Data.ToString.Basic

class ToString (α : Type u) :
Instances
    instance instToStringIdType {α : Type u_1} [ToString α] :
    Equations
    instance instToStringId {α : Type u_1} [ToString α] :
    Equations
    Equations
    Equations
    Equations
    • instToStringDecidable = { toString := fun h => match h with | isTrue h => "true" | isFalse h => "false" }
    def List.toString {α : Type u_1} [ToString α] :
    List αString
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance instToStringList {α : Type u} [ToString α] :
      Equations
      • instToStringList = { toString := List.toString }
      Equations
      instance instToStringULift {α : Type u} [ToString α] :
      Equations
      • instToStringULift = { toString := fun v => toString v.down }
      Equations
      Equations
      Equations
      Equations
      Equations
      instance instToStringFin (n : Nat) :
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        instance instToStringOption {α : Type u} [ToString α] :
        Equations
        instance instToStringSum {α : Type u} {β : Type v} [ToString α] [ToString β] :
        ToString (α β)
        Equations
        • One or more equations did not get rendered due to their size.
        instance instToStringProd {α : Type u} {β : Type v} [ToString α] [ToString β] :
        ToString (α × β)
        Equations
        instance instToStringSigma {α : Type u} {β : αType v} [ToString α] [(x : α) → ToString (β x)] :
        Equations
        • instToStringSigma = { toString := fun x => match x with | { fst := a, snd := b } => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩" }
        instance instToStringSubtype {α : Type u} {p : αProp} [ToString α] :
        Equations
        • instToStringSubtype = { toString := fun s => toString s.val }
        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.