[isabelle-dev] Subscripts within identifiers

[Gerwin Klein]

> So here is a reform that works with minimal impact on existing sources:
>
>  * Block sub/superscripts (\<^bsub>..\<^esub> and \<^bsup>..\<^esup>)
>    are not affected at all -- this is a different concept.
>
>  * There is just one \<^sub> and \<^sup> control symbol to that effect;
>    \<^isub> and \<^isup> remain within the infinite collection of
>    Isabelle symbols without any special meaning.
>
>  * \<^sub> and \<^sup> are no longer "letters".
>
>  * Superscript is for explicit notation, e.g. "x\<^sup>2" for some
>    operator "_\<^sup>2" applied to term x.
>
>  * Subscript may get used within identifiers, e.g. "x\<^sub>2" for a
>    variable of that name.
>
> The traditional ML identifier syntax is like this:
>
>  LETTER = A .. Z a .. Z
>  DIGIT = 0 .. 9
>  LETDIG = LETTER | DIGIT | _ | '
>
>  IDENTIFIER = LETTER LETDIG*
>
> So it is a strict letter followed by a sequence of liberal letters.
>
> Instead of making \<^sub> a "letter" as was done in Isabelle2003, the syntax is changed like this:
>
>  LETTER = A .. Z a .. Z \<alpha> ... \<A> ... \<a> ... etc.
>  DIGIT = 0 .. 9
>  LETDIG = LETTER | DIGIT | _ | '
>  SUBSCRIPT = \<^sub>
>
>  IDENTIFIER = LETTER ( SUBSCRIPT? LETDIG )*

Pairing up subscript and letdig is definitely a good idea.

One minor point:

I think we should allow

> IDENTIFIER = (SUBSCRIPT LETDIG)? LETTER ( SUBSCRIPT? LETDIG )*

i.e. allow a subscript at the beginning of an identifier. This is probably not used much (or at all) currently, but I've seen this plenty of times in maths texts. Or is there a good reason against it?

I'm less sure about the distinction between sub and sup. I can see it mostly aligns with current usage patterns, but I find this distinction even more confusing. Maybe that's just me and it's worth it if we can eliminate the isub/sub dimension. I can live with either, so I'll leave it to others to argue about it.

Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.