Why can't identifiers be named in other languages?

Stream: general

[Marvin]

I'm using Lean as a host for a multilingual linguistics project. (I don't simply mean that the team members speak different languages, I mean the point is providing encodings for multiple languages)

If I try to name an identifier in Korean for example, I'm finding that this is considered illegal

axiom α : Type
axiom 나 : α
--    ^ expected token

Is there a technical reason for this, or is it just social norms enforcement?

I see that «나» is legal, but I don't want to write this everywhere and I don't understand why such restriction is in place. Can this be disabled at least on a codebase opt-in?

[Malvin Gattinger]

I think there are some restrictions on which part of unicode is allowed in identifiers by default, but could not find them. That said, you can use notation to be allowed to write it without the « » later:

axiom α : Type
axiom «나» : α

notation "나" => «나»

example : 나 = 나 := by rfl

[Chris Bailey]

Malvin Gattinger said:

I think there are some restrictions on which part of unicode is allowed in identifiers by default, but could not find them.

This maybe?

[Aaron Liu]

I'm guessing it's a docs#Lean.isIdFirst followed by zero or more docs#Lean.isIdRest

[Yuyang Zhao]

#lean4 > Accept more Unicode in identifiers?