Zulip Chat Archive

Stream: general

Topic: superscripts in identifiers


Bernd Losert (Feb 18 2022 at 19:34):

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

Alex J. Best (Feb 18 2022 at 19:51):

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 (Feb 18 2022 at 19:52):

Numeric subscripts work.

Bernd Losert (Feb 18 2022 at 19:56):

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 (Feb 18 2022 at 19:57):

You can always use french quotes:

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

Yakov Pechersky (Feb 18 2022 at 19:58):

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

Yakov Pechersky (Feb 18 2022 at 19:58):

Via \f<<>>

Bernd Losert (Feb 18 2022 at 19:58):

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

Yury G. Kudryashov (Feb 18 2022 at 20:06):

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 (Feb 18 2022 at 20:06):

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

Gabriel Ebner (Feb 18 2022 at 20:20):

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 (Feb 18 2022 at 20:21):

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 (Feb 18 2022 at 20:22):

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 (Feb 18 2022 at 20:30):

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 (Feb 18 2022 at 20:35):

Are you sure?

Yury G. Kudryashov (Feb 18 2022 at 20:36):

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 (Feb 18 2022 at 20:41):

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 (Feb 18 2022 at 21:47):

Nfoobarm

Probably fails

Yury G. Kudryashov (Feb 18 2022 at 21:47):

Without spaces


Last updated: Dec 20 2023 at 11:08 UTC