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 (l : String) (r : α) => l ++ ", " ++ toString r) ("[" ++ toString x_1) xs).push ']'

@[implicit_reducible]

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

Equations

• instToStringList = { toString := List.toString }

@[implicit_reducible]

instance instToStringArray {α : Type u_1} [ToString α] : ToString (Array α)

Equations

• instToStringArray = { toString := fun (xs : Array α) => "#" ++ toString xs.toList }

@[implicit_reducible]

instance instToStringByteArray : ToString ByteArray

Equations

• instToStringByteArray = { toString := fun (bs : ByteArray) => bs.toList.toString }

@[implicit_reducible]

instance instToStringInt : ToString Int

Equations

• instToStringInt = { toString := Int.repr }