unicodeSymbol in stx?

Stream: lean4

[Thomas Murrills]

My understanding at the moment is that there’s no stx for unicodeSymbol—that is, you can’t write e.g. syntax foo := unicodeSymbol("←", "<-").

It appears like this would require a new constructor in ParserDescr and special handling during stx elaboration in toParserDescr. (It seems like it wouldn’t make sense as a parser alias, since the arguments of parser aliases are always expected to be arbitrary parsers, not e.g. strings.)

Is that understanding correct? If so, are there other technical obstacles to handling unicodeSymbol in stx?

Also, I imagine this is quite low-priority, but would it warrant an issue?