superscripts in identifiers

Stream: general

[Bernd Losert]

Are superscripts not supported in identifiers? I just tried def aᵉ : ℕ := 1 and it does not work.

[Alex J. Best]

https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/src/util/name.cpp#L28-L56 is the source code, as you can see it's not entirely simple to say what is and isn't valid. But not every unicode character is for sure.

[Yury G. Kudryashov]

Numeric subscripts work.

[Bernd Losert]

Interesting. There was a time when I thought that Lean's unicode support was as good as Agda's, but I guess not. If I make a PR with a is_sup_script_alnum_unicode, do you think it would get merged?

[Yakov Pechersky]

You can always use french quotes:

def «aᵉ» : ℕ := 1
#check «aᵉ»

[Yakov Pechersky]

def «my little nat» : ℕ := 1
#check «my little nat»

[Yakov Pechersky]

Via \f<<>>

[Bernd Losert]

Oh, I didn't know about the french quotes. Nice.

[Yury G. Kudryashov]

I guess, @Gabriel Ebner knows exactly what parts of Unicode are supported without french quotes and where to add more in the lean source.

[Alex J. Best]

You can also make notations for things you want to look a specific way rather than have them be identifiers

[Gabriel Ebner]

The reason this is not supported is because ᵉ should be notation. The official list of supported Unicode classes is here: https://github.com/leanprover-community/lean/blob/402f41cdedbd46a368fb7807bebe83550d887631/src/util/name.cpp#L27-L56

[Gabriel Ebner]

I'm happy to merge additions to the Lean 3 list iff they are added to Lean 4. (Please just stick to the current set of allowed identifiers.)

[Patrick Massot]

There is indeed a cost in supporting lot of unicode in identifier names. It makes things unusable as notations without putting spaces everywhere.

[Bernd Losert]

I didn't realize that you end up with problems regarding notation if you also allowed them as identifiers. I don't seem to have this problem when I define notation using normal ascii characters.

[Yury G. Kudryashov]

Are you sure?

[Yury G. Kudryashov]

Try

postfix `aaa`:100 := nat.succ
postfix `ᵉ`:100 := nat.succ

lemma baaa (n : ℕ) : naaa = n + 1 := rfl
lemma booo (n : ℕ) : nᵉ = n + 1 := rfl

[Bernd Losert]

Yeah, maybe it fails with postfix, but I can do this without problem:

notation x `foobar` y := (2 : nat)
def thefoobar : ℕ := (1 foobar 2)

[Yury G. Kudryashov]

Nfoobarm

Probably fails

[Yury G. Kudryashov]

Without spaces