List-like interface for `String`?

Stream: mathlib4

[Arien Malec]

I was looking at Mathlib.Data.String.Basic and it seems to be using a list-like API for String, with cons, head, etc.

It doesn't look like Lean 4 replicates that API (presumably b/c Unicode doesn't make these straightforward implementations)?

[Eric Wieser]

There'd be little point in String.head since it would just be a shorthand for String.data.head

[Eric Wieser]

docs#string.cons doesn't existing in mathlib3 either though so I'm not really sure what you're referring to

[Arien Malec]

Ah, in the first case, I was confused between the iterator and the string...

But string.head is referenced in mathlib.data.string.basic to_list_nonempty

[Arien Malec]

defined in mathlib.data.string.defs

[Arien Malec]

which is currently unported :-)

[Arien Malec]

I think it turns out to be an odd dependency issue for data.string.basic