Email Gateway (Aug 22 2022 at 14:54): Email Gateway (Aug 22 2022 at 14:54):From: Manuel Eberl <eberlm@in.tum.de>
Someone on Stack Overflow [1] just stumbled over the fact that you
cannot use the letter ‘o’ as an identifier in Isabelle terms. Of course,
this is due to its being the ASCII syntax for Fun.comp.
Is there still any necessity for this notation? If not, I suggest
removing it and also ‘O’ and perhaps even ‘OO’, since this just confuses
people needlessly in my opinion.
Cheers,
Manuel
[1] http://stackoverflow.com/questions/41560374
Email Gateway (Aug 22 2022 at 14:54):From: David Cock <david.cock@inf.ethz.ch>
Manuel,
It is a bit annoying yes. There should definitely by some syntax for
function and relation composition - it really should be possible to
write it compactly.
David
Email Gateway (Aug 22 2022 at 14:54):From: Peter Lammich <lammich@in.tum.de>
It is a bit annoying yes. There should definitely by some syntax
for
function and relation composition - it really should be possible to
write it compactly.
for function composition, we have \<circ>.
Afaik, there is no non-ASCII syntax for relcomp.
Email Gateway (Aug 22 2022 at 14:54):From: Lawrence Paulson <lp15@cam.ac.uk>
These ASCII notations are slowly fading away and I think that this one can go as well.
Relational composition complicates matters. I don’t think is a simple way to use \circ in both roles. Can anyone come up with a proposal?
Larry Paulson
Email Gateway (Aug 22 2022 at 14:54):From: David Cock <david.cock@inf.ethz.ch>
There's \<circle>.
David
Email Gateway (Aug 22 2022 at 14:55):From: Tobias Nipkow <nipkow@in.tum.de>
I would not use up \<circle> because that is the Next operator in temporal logic.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 14:55):From: Christian Sternagel <c.sternagel@gmail.com>
Just some further possibilities:
\<cdot> (I'm not sure whether this is used anywhere else---except of
course in IsaFoR, where it is substitution application)
or adhoc overloading to reuse \<circ>
cheers
chris
Email Gateway (Aug 22 2022 at 14:55):From: David Cock <david.cock@inf.ethz.ch>
True, bold circ and cdot a both better choices.
David
Email Gateway (Aug 22 2022 at 14:56):From: Peter Gammie <peteg42@gmail.com>
On 11 Jan 2017, at 00:31, Christian Sternagel <c.sternagel@gmail.com> wrote:
Just some further possibilities:
- \<^bold>\<circ>
- \<cdot> (I'm not sure whether this is used anywhere else---except of
course in IsaFoR, where it is substitution application)
It’s used in HOLCF for continuous function application.
- or adhoc overloading to reuse \<circ>
Sounds OK to me if it can be made to work.
I don’t know much about why Isabelle’s non-ASCII symbols are as they are, but why are we stuck using names like \<circ>? How about introducing \<comp> (function) and \<Comp> (relation) symbols and mapping these to whatever pleasing visual symbols are available?
cheers,
peter
Email Gateway (Aug 22 2022 at 14:56):From: Makarius <wenzelm@in.tum.de>
Isabelle symbols follow certain concepts that are explained in the
canonical documentation.
While the concept of Isabelle symbols has been quite stable in the past
decades, input methods have changed constantly.
The 'abbrevs' declaration in a theory header makes it easy to introduce
library-specific ways to write arbitrary text (including symbol
agglomerates).
There are already some example uses in Isabelle2016-1.
Makarius
Last updated: May 07 2024 at 04:19 UTC