Emoji as variable names

Stream: general

[Martin Dvořák]

Is it possible to use emoji as variable names without the french quotation marks?

example («🐶» «🐱» : Nat) : «🐶» + «🐱» = «🐱» + «🐶» :=
  Nat.add_comm «🐶» «🐱»

I would like to be able to write:

example (🐶 🐱 : Nat) : 🐶 + 🐱 = 🐱 + 🐶 :=
  Nat.add_comm 🐶 🐱

Is there any project-wide settings that I could use, even if it means enumerating all allowed symbols ahead of time?

[Johan Commelin]

I think you can't easily change what identifiers can look like. But you could hack together an elaborator/delaborator pair that converts between 🐶 and emoji_🐶.

[Martin Dvořák]

Yeah but emoji_🐶 needs to be frenchquoted, too.

[Johan Commelin]

Sure, the elaborator can do that for you.

[Edward van de Meent]

doesn't this need to happen at tokenization instead of at elaboration?