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 instToStringSubstring : ToString Substring

instance instToStringIterator : ToString String.Iterator

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 instToStringPos : ToString String.Pos

instance instToStringInt : ToString Int

instance instToStringChar : ToString Char

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)

def String.toInt? (s : String) : Option Int

Interprets a string as the decimal representation of an integer, returning it. Returns none if the string does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit and optionally - in front. Leading + characters are not allowed.

Use String.isInt to check whether String.toInt? would return some. String.toInt! is an alternative that panics instead of returning none when the string is not an integer.

Examples:

• "".toInt? = none
• "-".toInt? = none
• "0".toInt? = some 0
• "5".toInt? = some 5
• "-5".toInt? = some (-5)
• "587".toInt? = some 587
• "-587".toInt? = some (-587)
• " 5".toInt? = none
• "2-3".toInt? = none
• "0xff".toInt? = none

def String.isInt (s : String) : Bool

Checks whether the string can be interpreted as the decimal representation of an integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit and optionally - in front. Leading + characters are not allowed.

Use String.toInt? or String.toInt! to convert such a string to an integer.

Examples:

• "".isInt = false
• "-".isInt = false
• "0".isInt = true
• "-0".isInt = true
• "5".isInt = true
• "587".isInt = true
• "-587".isInt = true
• "+587".isInt = false
• " 5".isInt = false
• "2-3".isInt = false
• "0xff".isInt = false

def String.toInt! (s : String) : Int

Interprets a string as the decimal representation of an integer, returning it. Panics if the string does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit and optionally - in front. Leading + characters are not allowed.

Use String.isInt to check whether String.toInt! would return a value. String.toInt? is a safer alternative that returns none instead of panicking when the string is not an integer.

Examples:

• "0".toInt! = 0
• "5".toInt! = 5
• "587".toInt! = 587
• "-587".toInt! = -587

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

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