kmill
commented
9 months ago Here is some previous Zulip discussion where @digama0 investigated what's allowed in identifiers. I think there was another thread too, but I couldn't quickly locate it.
Open madvorak opened 9 months ago
kmill
commented
9 months ago Here is some previous Zulip discussion where @digama0 investigated what's allowed in identifiers. I think there was another thread too, but I couldn't quickly locate it.
Proposal
Allow the symbol
ⱼto appear in identifiers without the need of French quotes.User Experience: I believe this feature will slightly improve the aesthetics of some code written in Lean. It is unfortunate that Unicode doesn't have subscript characters for all letter from the Latin alphabet. Nevertheless, it would be good to have as many subscript characters as possible. Currently
ⱼis supported by both Unicode and the VS Code extension but not by Lean.Beneficiaries: Mathematicians who are used to naming variables
xⱼwill like that they don't have to change their notation in this case. On the other hand, I am bit worried it might slightly slow down the lexing of all Lean code (even whenⱼis not present in it).Maintainability: This will probably worsen code maintenance, as
ⱼis not in the same interval as other subscript characters in Unicode.Community Feedback
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20.E2.B1.BC.20.28U.2B2C7C.29.20in.20identifiers
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.