superscript π?

[Julian Bradfield]

On 2021-08-02, Matt Rice via Unicode <unicode at corp.unicode.org> wrote:
> 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.

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

Equally, it's not a good argument for characters if tool writers can't
be bothered to implement simple HTML-style display of things that must
internally be structured data anyway. Though as far as I see in Lean,
the scripts have no meaning; it's just that identifiers can contain
subscript characters. You can just as well name your variable g_1 (or
g1) as g₁. I'm curious what forced you to use a subscript.

(Long ago, I made quite a fancy display mode for maths in Emacs. After
a few years, I stopped using it. Nowadays I use Unicode, but only when
writing email to students who might not yet be familiar with LaTeX.)