Email Gateway (Aug 19 2022 at 11:46): Email Gateway (Aug 19 2022 at 11:46):From: Peter Lammich <lammich@in.tum.de>
With the new semanmtics, is there any way to get notation that works by
subscripting letters. I have no idea how to port the following two
notations, that I'm using quite frequently:
abbreviation is_LINEAR ("_\<^sub>L") where "x\<^sub>L == LIN_ANNOT x
LINEAR"
abbreviation is_NON_LINEAR ("_\<^sub>N") where "x\<^sub>N == LIN_ANNOT x
NON_LINEAR"
Any hints,
Peter
Email Gateway (Aug 19 2022 at 11:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
The problem should only occur if you annotate an identifier (i.e., a variable or a
constant), but not for compound terms. If you make sure that \<^sub>L does not directly
follow an identifier, then your notation still works. For example, you can write the
following:
x \<^sub>L
(x)\<^sub>L
If you do not like the parentheses or the spaces, you can abuse bsub/esub as follows, but
this is not what bsub/esub originally were meant for.
abbreviation is_LINEAR ("_\<^bsub>L\<^esub>")
where "x\<^bsub>L\<^esub> == LIN_ANNOT x LINEAR"
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 11:47):From: Peter Lammich <lammich@in.tum.de>
Thanks for this hint ... however, I chose to change my annotations to
superscripts, that still work as usual.
Email Gateway (Aug 19 2022 at 11:47):From: Makarius <makarius@sketis.net>
As usual, Andreas is fully up-to-date concerning the state-of-the-art with
sub/subscript identifiers vs. notation, probably based on careful reading
of incoming changesets of the main Isabelle repository and AFP.
I would give both approaches above a > 50% rating. They are not perfect,
but not so bad. \<^bsub>..\<^esub> has indeed a specific meaning for
optional term arguments in notation that depends on a "structure".
HOL-Algebra has many examples of its regular use. A second use as
fall-back notation as above is OK. In Isabelle/jEdit you won't see an
actual subscript, though.
(Somehow this thread got displaced on isabelle-users, which is about
official Isabelle releases, not arbitrary Isabelle repository snapshots.
We are still 3-4 weeks before any public release candidates of
Isabelle2013-1, which will be announced here. The official launch of
Isabelle2013-1 is anticipated for early November 2013.)
Makarius
Email Gateway (Aug 19 2022 at 11:47):From: Makarius <makarius@sketis.net>
That is also a way, and conforms better to the idea behind it: subscript
for identifiers, superscript for notation.
"Works as usual" should not be a guiding principle, just because something
works accidentally a certain way over a certain period of time. The
ongoing homeopathic changes of Isabelle behaviour are meant to converge to
the Right Thing eventually, hopefully without major set backs.
(This detail about sub/superscripts is only relevant for the coming
Isabelle2013-1 release to emerge this Fall.)
Makarius
Last updated: Apr 26 2024 at 16:20 UTC