Email Gateway (Aug 18 2022 at 20:23): Email Gateway (Aug 18 2022 at 20:23):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
is it possible to remove an abbreviation. Currently I am using an
auxiliary context
context
fixes P :: "'a => 'a => bool"
begin
...
in order to fix the parameter (P) of another definition during document
preparation.
Thus I defined syntax for P (via notation) as well as the abbreviation
abbreviation notP :: "'a => 'a => bool" where
"notP x y == not P x y"
also with special syntax.
However, after closing the context, the abbreviation is still active and
but turns out to be too general, since, e.g., "~ (x = y)" is now also
printed "notP (op =) x y", which was not intended. Any advise?
cheers
chris
Email Gateway (Aug 18 2022 at 20:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I guess the situation is similar to thread »syntax in auxiliary
contexts«: the handling of syntax declaration wrt. to the context
sandwich still needs fine tuning.
Apart from that, there is no way to remove an abbreviation:
abbreviations are managed monotonously.
Cheers,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC