[isabelle-dev] Subscripts within identifiers
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
>> 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
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