Unicode in string literals

Stream: lean4

[Eric Wieser]

What's the syntax for creating a Char from a non-bmp unicode offset?

#eval '\u0061' -- ok
#eval '\u1F300' -- syntax error
#eval '\U0001F300' -- syntax error

[Kyle Miller]

There's no syntax for that at the moment beyond "🌀"

[Damiano Testa]

You can also use #eval Char.ofNat 0x1f300 :smile:

[Eric Wieser]

I threw together a draft at lean4#5443, but I guess that needs an RFC and tests