unicode segmentation

Stream: Is there code for X?

[Alok Singh]

like the rust crate, or bindings to it. i've often used its .graphemes() method to get arrays of characters for easier-to-think-about parsing rather than raw utf8 strings

[Eric Wieser]

I assume you are aware that there is a middle ground between "raw UTF8 strings" and "sequences of grapheme clusters", which is "sequences of unicode codepoints" (and supported in Lean natively)?

[Eric Wieser]

https://github.com/fgdorais/lean4-unicode-basic is probably the most sophisticated unicode processing that currently exists in Lean.