Email Gateway (Aug 19 2022 at 09:08): Email Gateway (Aug 19 2022 at 09:08):From: Makarius <makarius@sketis.net>
Type => and \<lambda> is also "metalogic" in your categorisation, also the
"::" notation for type and sort constraints. Isabelle/HOL re-uses the
Pure type system for its purposes. Pure notation has rather low syntax
priorities, which explains why it is all at the bottom of your list.
Makarius
Email Gateway (Aug 19 2022 at 09:19):From: Holger Blasum <hbl@sysgo.com>
Dear all,
attached is an attempt to follow-up on last week's discussion (thanks!). I
think it is good enough for myself at the moment, however in case
sth like this would make it into user documentation note that there
are still some gaps e.g. concerning precedence values e.g. of "set"/"list"
type constructors or the application of user-defined functions.
Best,
isabelle-operator-precedence-cheat-sheet.pdf
isabelle-operator-precedence-cheat-sheet.tex
Email Gateway (Aug 19 2022 at 09:31):From: Tobias Nipkow <nipkow@in.tum.de>
You have prompted me to add a table of infix operators to the existing "What's
in Main" manual (development version). In the process I have also fixed a few
odd associativities, mostly making a few predicates non-associative. The table
differs from yours in a number of respects. I am still debating if the framework
operators like ==> should be in there too, although they come not from HOL but Pure.
Thanks for your prompt.
Tobias
Email Gateway (Aug 19 2022 at 09:32):From: Arthur Peters <amp@singingwizard.org>
<delurk>
As a current learner of Isabelle: Please include the Pure operators
(though marking them as not from HOL makes sense). I think this is
important because they appear mixed with HOL operators frequently, so
having it all in one place is useful and avoids confusion. Just
because an operator is actually from the underlying Pure does not
change the fact that it is part of the normal HOL style and workflow,
so it still belongs in such a list. Also it's useful for comparison
with the HOL operators.
</delurk>
-Arthur
Email Gateway (Aug 19 2022 at 09:32):From: Holger Blasum <hbl@sysgo.com>
Hi Tobias,
Thanks for doing this! Looking at
http://isabelle.in.tum.de/repos/isabelle/diff/0eaefd4306d7/src/Doc/Main/Main_Doc.thy and given that you asked for feedback (on Pure)
I'm wondering why they are ordered in this way (maybe the list
is automatically generated which would be good from a
maintainability perspective), otherwise perhaps just order them
ascending or descending and perhaps add a sentence ``functions
always beat relations, relations always beat HOL logic symbols,
HOL logic symbols always beat Pure'' (maybe I'm oversimplifying ...)
If the list is autogenerated then just write that (so a reader
does not have to try to discover any meaning ...). Or briefly explain the
other ordering principle you applied.
I'd also second Arthur that Pure would be nice to have too (unless
it is already elsewhere). In case sb knows it: user-defined functions
are at 100 or 1000?
best,
Email Gateway (Aug 19 2022 at 09:33):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Currently the appendix of the »old« Isabelle/HOL tutorial has a similar
purpose. Maybe this is a candidate for unification.
Florian
signature.asc
Last updated: Apr 25 2024 at 01:08 UTC