[isabelle-dev] Subscripts within identifiers
noschinl at in.tum.de
Tue Jul 2 15:55:50 CEST 2013
On 02.07.2013 13:15, Makarius wrote:
> After 10 years we actually have a chance to stop such jokes about
> identifiers starting or ending with control symbols, or control
> symbols getting out of sync, and especially the confusion about which
> of the two subscript controls is what.
What do you mean by "getting out of sync" in contrast to
"starting/ending with control symbols"?
> * 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.
I.e., in the notation below they are not are LETTERs anymore and the
then-current IDEs will stop rendering them as sub-/superscripts?
> * Superscript is for explicit notation, e.g. "x\<^sup>2" for some
> operator "_\<^sup>2" applied to term x.
Graph_Theory/Digraph from the AFP defines a constant reachable
("_ \<rightarrow>\<^isup>*\<index> _" [100,100] 40)
(this should probably by "infix" instead). Is this going to stay
valid (with \<^isup> replaced by \<^sup>)? It does not quite fit the
scheme you described above.
> * Subscript may get used within identifiers, e.g. "x\<^sub>2" for a
> variable of that name.
This proposal excludes superscripts from occurring in identifiers. Does
this mean that there was no legitimate use of \<isup> at all?
> 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 )*
[ I always assumed the "_" was also excluded from occurring at the end
of a (parsed) identifier? ]
More information about the isabelle-dev