Re: superscript π?

[Matt Rice]

On Sun, Aug 1, 2021 at 1:56 PM Julian Bradfield via Unicode
<unicode at corp.unicode.org> wrote:
>
> On 2021-08-01, David Chmelik via Unicode <unicode at corp.unicode.org> wrote:
> > less-common cases there is notation for that.  In the more common cases
> > of just one level, scientists are tired of having to use other notation.
>
> Do you have evidence for that? I've never interacted with a scientist
> who would rather remember how to type a superscript unicode character
> than type ^.

I haven't looked through all the uses of superscripts and subscripts
in the lean theorem prover or mathlib,
But I know they get used there somewhat frequently, and I myself at
least once had to rename a variable to one which had a subscript
from a character which did not.

Looking through the mathlib library in alphabetical order, the first
file I opened contains many, I've highlighted some
https://github.com/leanprover-community/mathlib/blob/master/src/algebra/algebra/basic.lean#L407-L412

As far as remembering unicode characters, when editing lean you would
typically use the abbreviations file
rather than entering unicode characters directly, so \^ or \_.  I
don't really think editor or keymap interaction is
good argument either for or against any specific character.

Abbreviations for superscript/subscript characters in the editor
highlighted (To enter the abbreviation you would prefix the character
sequence with a '\')
https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json#L1150-L1316

>From this perspective of picking variable names and eventually wanting
superscript/subscript coverage for that variable I'd imagine the more
coverage the better,
and I doubt anyone coming from lean would argue against wider
coverage...  my 2c...