Email Gateway (Aug 18 2022 at 13:16): Email Gateway (Aug 18 2022 at 13:16):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello
Is there any way to modify/delete the syntax defined for some constants
that one imports from another theory?
I import some theory and would like to place the binding level of most
of my syntax between two constants which are declared using the same
priority.
smime.p7s
Email Gateway (Aug 18 2022 at 13:16):From: Peter Lammich <peter.lammich@uni-muenster.de>
Christian Doczkal wrote:
Have you tried using the
no_notation
declaration ?
Email Gateway (Aug 18 2022 at 13:18):From: Makarius <makarius@sketis.net>
On Thu, 2 Apr 2009, Dr. Brendan Patrick Mahony wrote:
Regarding no_syntax and no_notation, they have the provoking property
that it is hard to get the revoked syntax to stay revoked.
This happens uniformly for all global declarations (at the immediate
theory level), e.g. declare foo [simp del]
Or else the theory import could be a bit smarter and not merge in a
theory that is imported by another imported theory.
Locales already work differently: instead of maintaining (and merging)
data, they manage declarations on data (update functions). So here you
would get a potentially more convenient behaviour: the last declaration of
notation or no_notation will take effect.
I have occasionally pondered the question if one could achieve a similar
mode of operation at the global level as well, without breaking every
existing theory out there.
If you unthinkingly include Set.thy, or anything else that directly
imports Set.thy, all the ugly notation is right back where you don't
want it. This means you frequently can't use the imports list that best
describes or hints at the subject matter of a new theory.
Normally you should never import anything below theory Main, or you will
inevitably participate in the quite delicate bootstrap process of Main
HOL. Strange effects can happen when primitive theories of HOL are merged
via different paths.
Makarius
Email Gateway (Aug 18 2022 at 13:22):From: "Dr. Brendan Patrick Mahony" <brendan.mahony@dsto.defence.gov.au>
Regarding no_syntax and no_notation, they have the provoking property
that it is hard to get the revoked syntax to stay revoked. If you
unthinkingly include Set.thy, or anything else that directly imports
Set.thy, all the ugly notation is right back where you don't want it.
This means you frequently can't use the imports list that best
describes or hints at the subject matter of a new theory. At least
this was true in Isabelle 2005. Is it still true in the 2008 version?
In the latest builds?
Perhaps rather than removing it from grammar it could be added to a
deprecated production list or something?
Or else the theory import could be a bit smarter and not merge in a
theory that is imported by another imported theory.
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
Last updated: May 03 2024 at 12:27 UTC