@[reducible, inline]

abbrev Std.Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β] (it : Iter β) : List String

Convenience function for turning an iterator into a list of strings, provided the output of the iterator implements ToString.

Equations

• it.toStringList = (Std.Iter.map toString it).toList

@[reducible, inline]

abbrev Std.Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β] (it : Iter β) : Array String

Convenience function for turning an iterator into an array of strings, provided the output of the iterator implements ToString.

Equations

• it.toStringArray = (Std.Iter.map toString it).toArray