Display of List.toString

Stream: lean4

[Paige Thomas]

I was expecting a display of "a", but I get "[a]".

set_option autoImplicit false

#eval List.toString ['a']

[Kyle Miller]

List.toString is the implementation of the ToString class for List. That's behaving as expected.

What behavior are you looking for? Maybe this?

#eval String.join (List.map toString ['a'])

[Paige Thomas]

ahh, yes, thank you.

[Paige Thomas]

Actually, I think what I wanted was List.asString.

[Paige Thomas]

Which may do the same thing.