unsupported unicode

Stream: lean4

[Jihoon Hyun]

The unicode for double tack (⫫ : U+2AEB) is not supported.
Is there a list of unicodes supported in lean?

[Eric Wieser]

Works for me:

notation "⫫" => 0
#check ⫫

[Eric Wieser]

What do you mean by "unsupported"?

[Jihoon Hyun]

I meant that it couldn't be used as a variable like \alpha. Although after looking at your answer, I thought it is definitely not a variable..

[Jon Eugster]

Do you mean that the following things don't work:

variable (⫫ : ℕ)    -- error: expected token
variable (ˣ : ℕ)    -- error: expected token
variable (₁s : ℕ)   -- error: expected token

I wanna say that variable names are of type Lean.Name and not everything is allowed in them. However, I wouldn't know how I'd find out what the rules are.

[Eric Wieser]

variable («⫫» : ℕ)    -- ok
variable («ˣ» : ℕ)    -- ok
variable («₁s» : ℕ)   -- ok

[Mario Carneiro]

there is a specific set of unicode codepoints allowed in identifiers without quoting, basically alphabetic characters in several languages plus letter-like symbols

[Mario Carneiro]

https://github.com/leanprover/lean4/blob/510bc47cc366e7d231c62c31f7ec1cbbacda9e6d/src/Init/Meta.lean#L71-L77