[isabelle-dev] Subscripts within identifiers

[Makarius]

On Tue, 2 Jul 2013, Gerwin Klein wrote:

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

Can you show such math texts?  I can't remember having seen this recently.

In any case, exotic notation can always be introduced via mixifx notation 
for particular identifiers: global constants or locally fixed variables, 
but excluding bound variables.


> Or is there a good reason against it?

A strict LETTER as the start of identifiers makes the token language more 
robust. Subscript often appears at the end of some notation, so it could 
be in conflict to determine the identifier boundary.

I have seen situations of variations of arrows for certain parameterized 
relations like this:

   x -->\<^sub>a y  ==  x --> a y

where "-->\<^sub>a" and "-->" are literal tokens for two different mixfix 
forms.

This can cause confusion of \<^sub>a would become a legal identifier, 
depending how spaces are put in the input.  Right now it still works, due 
to the separation of \<^sub> for notation and \<^isub> for identifiers -- 
assuming users still adhere to this old principle in the first place.


 	Makarius