[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Mon Jul 15 12:18:47 CEST 2013
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
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
More information about the isabelle-dev