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 α)

Equations

• instToStringId = inferInstanceAs (ToString α)

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

Equations

• instToStringId_1 = inferInstanceAs (ToString α)

instance instToStringString : ToString String

Equations

• instToStringString = { toString := fun (s : String) => s }

instance instToStringSubstring : ToString Substring

Equations

• instToStringSubstring = { toString := fun (s : Substring) => s.toString }

instance instToStringIterator : ToString String.Iterator

Equations

• instToStringIterator = { toString := fun (it : String.Iterator) => it.remainingToString }

instance instToStringBool : ToString Bool

Equations

• instToStringBool = { toString := fun (b : Bool) => bif b then "true" else "false" }

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

Equations

• instToStringDecidable = { toString := fun (h : Decidable p) => match h with | isTrue h => "true" | isFalse h => "false" }

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, ]"

Equations

• [].toString = "[]"
• [x_1].toString = "[" ++ toString x_1 ++ "]"
• (x_1 :: xs).toString = (List.foldl (fun (x1 : String) (x2 : α) => x1 ++ ", " ++ toString x2) ("[" ++ toString x_1) xs).push ']'

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

Equations

• instToStringList = { toString := List.toString }

instance instToStringPUnit : ToString PUnit

Equations

• instToStringPUnit = { toString := fun (x : PUnit) => "()" }

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

Equations

• instToStringULift = { toString := fun (v : ULift α) => toString v.down }

instance instToStringUnit : ToString Unit

Equations

• instToStringUnit = { toString := fun (x : Unit) => "()" }

instance instToStringNat : ToString Nat

Equations

• instToStringNat = { toString := fun (n : Nat) => n.repr }

instance instToStringPos : ToString String.Pos

Equations

• instToStringPos = { toString := fun (p : String.Pos) => p.byteIdx.repr }

instance instToStringInt : ToString Int

Equations

• instToStringInt = { toString := fun (x : Int) => match x with | Int.ofNat m => toString m | Int.negSucc m => "-" ++ toString m.succ }

instance instToStringChar : ToString Char

Equations

• instToStringChar = { toString := fun (c : Char) => c.toString }

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

Equations

• instToStringFin n = { toString := fun (f : Fin n) => toString ↑f }

instance instToStringUInt8 : ToString UInt8

Equations

• instToStringUInt8 = { toString := fun (n : UInt8) => toString n.toNat }

instance instToStringUInt16 : ToString UInt16

Equations

• instToStringUInt16 = { toString := fun (n : UInt16) => toString n.toNat }

instance instToStringUInt32 : ToString UInt32

Equations

• instToStringUInt32 = { toString := fun (n : UInt32) => toString n.toNat }

instance instToStringUInt64 : ToString UInt64

Equations

• instToStringUInt64 = { toString := fun (n : UInt64) => toString n.toNat }

instance instToStringUSize : ToString USize

Equations

• instToStringUSize = { toString := fun (n : USize) => toString n.toNat }

instance instToStringFormat : ToString Std.Format

Equations

• instToStringFormat = { toString := fun (f : Std.Format) => f.pretty }

def addParenHeuristic (s : String) : String

Equations

• addParenHeuristic s = if ("(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s) = true then s else if (!s.any Char.isWhitespace) = true then s else "(" ++ s ++ ")"

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

Equations

• instToStringOption = { toString := fun (x : Option α) => match x with | none => "none" | some a => "(some " ++ addParenHeuristic (toString a) ++ ")" }

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

• instToStringProd = { toString := fun (x : α × β) => match x with | (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")" }

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

Equations

• instToStringSigma = { toString := fun (x : Sigma β) => match x with | ⟨a, b⟩ => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩" }

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

Equations

• instToStringSubtype = { toString := fun (s : Subtype p) => toString s.val }

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

Equations

• s.toInt? = if s.get 0 = '-' then do let v ← (s.toSubstring.drop 1).toNat? pure (-Int.ofNat v) else Int.ofNat <$> s.toNat?

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

Equations

• s.isInt = if s.get 0 = '-' then (s.toSubstring.drop 1).isNat else s.isNat

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

Equations

• s.toInt! = match s.toInt? with | some v => v | none => panic "Int expected"

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

Equations

• instToStringExcept = { toString := fun (x : Except ε α) => match x with | Except.error e => "error: " ++ toString e | Except.ok a => "ok: " ++ toString a }

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.