[isabelle-dev] Subscripts within identifiers

Makarius makarius at sketis.net
Fri Jul 5 13:52:03 CEST 2013

On Tue, 2 Jul 2013, Gerwin Klein wrote:

> I think we should allow
> 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 

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.


More information about the isabelle-dev mailing list