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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
