Re: superscript π?

[Matt Rice]

On Mon, Aug 2, 2021 at 2:58 PM Julian Bradfield via Unicode
<unicode at corp.unicode.org> wrote:
>
> 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.

I didn't write the linked code, but

It is a theorem prover for machine checked proofs, not a format intended for
displaying equations for which there are other things.
These can be long and tedious and involve many variables derived from
other variables...
Nothing "forced" me to use a subscript, it came about through a
refactoring for clarity in an effort to get rid of long largely
uninformative variables
like hnm1 hmn1 hnm2 hmn2.   But also because things such as a
functions inverse are most naturally conveyed by identifiers f⁻¹...

Unlike _ ^ isn't a valid identifier... Keeping the core implementation
of the language small and allowing unicode identifiers gives a good
balance between simplicity,
while affording some more opportunity for proof clarity (This is at
least what I imagine to be the case, I didn't implement the language
either)...

You asked for evidence. I offered some, There is plenty of evidence
that you _can_ do without subscripts and superscripts in theorem
provers that only support ascii identifiers...
yet people are clearly using sub/superscripts anyways when they are available.