[isabelle-dev] Subscripts within identifiers

[Makarius]

On Sat, 13 Jul 2013, Tjark Weber wrote:

> On Fri, 2013-07-12 at 19:41 +0200, Makarius wrote:
>> How would "Omega Algebras" fare with notation A\<^sup>\<infinity> instead
>> of A\<^sup>\<omega>?
>
> Worse. Of course, a name is just that, but for clarity and convenience, 
> it is nice to be able to call things in Isabelle what they are called in 
> the literature. For serious output (e.g., papers), A\<^sup>\<infinity> 
> instead of A\<^sup>\<omega> would demand further post-processing.

Printing papers is yet a slightly different thing.  One could play the 
usual "LaTeX sugar" tricks just for output, with alternative notation 
etc., or postprocess sources via some bits of perl in the document/build 
script (which is optional, and not there by default).


We should get a feeling for the tendency of the move.  At the start of the 
thread I claimed that \<^sup>LETDIG tends to be used in postfix notation, 
so the idea was to allow only \<^sub>LETDIG in identifiers.

Some people had a feeling that symmetry is better, and the empirical check 
revealed that \<omega> happens to be the only letter in conflict -- 
superscripted digits are usually done with old-fashioned \<twosuperior> 
etc.  (In fact, the use of \<omega> is like that of a special numeral 
here.)


I am presently tending towards the symmetric sub/sup version, since it is 
a bit more conservative.

If we would go the other way, there would be also a reason to discontinue 
\<twosuperior> etc. eventually, but I did not intend such a reform right 
now.


 	Makarius