class ToString (α : Type u) : Type u

Types that can be converted into a string for display.

There is no expectation that the resulting string can be parsed back to the original data (see Repr for a similar class with this expectation).

• toString : α → String

  Converts a value into a string.

instance instToStringId {α : Type u_1} [ToString α] : ToString (id α)

instance instToStringId_1 {α : Type u_1} [ToString α] : ToString (Id α)

instance instToStringString : ToString String

instance instToStringRaw : ToString Substring.Raw

instance instToStringChar : ToString Char

instance instToStringBool : ToString Bool

instance instToStringDecidable {p : Prop} : ToString (Decidable p)

def List.toString {α : Type u_1} [ToString α] : List α → String

Converts a list into a string, using ToString.toString to convert its elements.

The resulting string resembles list literal syntax, with the elements separated by ", " and enclosed in square brackets.

The resulting string may not be valid Lean syntax, because there's no such expectation for ToString instances.

Examples:

• [1, 2, 3].toString = "[1, 2, 3]"
• ["cat", "dog"].toString = "[cat, dog]"
• ["cat", "dog", ""].toString = "[cat, dog, ]"

instance instToStringList {α : Type u} [ToString α] : ToString (List α)

instance instToStringPUnit : ToString PUnit

instance instToStringULift {α : Type u} [ToString α] : ToString (ULift α)

instance instToStringUnit : ToString Unit

instance instToStringNat : ToString Nat

instance instToStringRaw_1 : ToString String.Pos.Raw

instance instToStringInt : ToString Int

instance instToStringFin (n : Nat) : ToString (Fin n)

instance instToStringUInt8 : ToString UInt8

instance instToStringUInt16 : ToString UInt16

instance instToStringUInt32 : ToString UInt32

instance instToStringUInt64 : ToString UInt64

instance instToStringUSize : ToString USize

instance instToStringFormat : ToString Std.Format

def addParenHeuristic (s : String) : String

instance instToStringOption {α : Type u} [ToString α] : ToString (Option α)

instance instToStringSum {α : Type u} {β : Type v} [ToString α] [ToString β] : ToString (α ⊕ β)

instance instToStringProd {α : Type u} {β : Type v} [ToString α] [ToString β] : ToString (α × β)

instance instToStringSigma {α : Type u} {β : α → Type v} [ToString α] [(x : α) → ToString (β x)] : ToString (Sigma β)

instance instToStringSubtype {α : Type u} {p : α → Prop} [ToString α] : ToString (Subtype p)

instance instToStringExcept {ε : Type u_1} {α : Type u_2} [ToString ε] [ToString α] : ToString (Except ε α)

instance instReprExcept {ε : Type u_1} {α : Type u_2} [Repr ε] [Repr α] : Repr (Except ε α)