Documentation

Init.Data.ToString.Basic

class ToString (α : 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.

Instances

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 :

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 :

Equations

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

instance instToStringULift {α : Type u} [ToString α] :

ToString (ULift α)

Equations

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

instance instToStringUnit :

Equations

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

instance instToStringNat :

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 :

Equations

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

instance instToStringChar :

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 :

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 :

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

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

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 is not empty, its first character is either '-' or a digit, and all remaining characters are digits.

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
"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) :

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 is not empty, its first character is '-' or a digit, and all subsequent characters are digits. Leading + characters are not allowed.

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

Examples:

"".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) :

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 is not empty, its first character is '-' or a digit, and all remaining characters are digits.

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.