Re: superscript π?

Matt Rice ratmice at
Mon Aug 2 09:09:22 CDT 2021

On Sun, Aug 1, 2021 at 1:56 PM Julian Bradfield via Unicode
<unicode at> wrote:
> On 2021-08-01, David Chmelik via Unicode <unicode at> 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

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 '\')

>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...

More information about the Unicode mailing list