[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Fri Jul 5 17:49:55 CEST 2013
On Fri, 5 Jul 2013, Tobias Nipkow wrote:
> Am 05/07/2013 14:08, schrieb Makarius:
>> When I seen "x subscripted 2" it is by default an identifier, but "x
>> superscripted 2" is x-squared.
> I think this is not a good example. If you write "x\<isup>2" now it is an
> identifier and if you write "x\<^sup>2" it is illegal. If you refer to
> "x\<twosuperior>", that is a hack (but you could still write it).
Yes, that is a correct observation, and some minor additional confusion
that I did not intend to address here: ISO-Latin has special characters
for some superscripted digits, and unicode completes that to 0..9 (but we
are not using them right now). So the overlap could be limited to
\<^sup>LETTER, without \<^sup>DIGIT.
I will make another empirical test to see what happens -- but this always
takes hours (sometimes days) to get past small surprises.
More information about the isabelle-dev