Akim Demaille wrote:
Here, you are suggesting to use the same convention for both types of symbols? I’m ok with that move, but wouldn’t that cause some confusion for some users, especially beginners?
Yes, probably. I hadn't thought it through as carefully as you have. So let's leave them uppercase.
