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) => Substring.Internal.toString s }

instance instToStringChar : ToString Char

Equations

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

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

• One or more equations did not get rendered due to their size.
• [].toString = "[]"
• [x_1].toString = String.Internal.append (String.Internal.append "[" (toString x_1)) "]"

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 => String.Internal.append "-" (toString m.succ) }

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

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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.