Email Gateway (Aug 18 2022 at 13:02): Email Gateway (Aug 18 2022 at 13:02):From: Chris Capel <pdf23ds@gmail.com>
Is there a way to temporarily enable/disable syntax declared on
datatype constructors? I assume it would be done with no_syntax or
no_translations, but I'm not sure how.
I just tried a no_translations declaration, and that didn't seem to
work. I'm not sure what the no_syntax declaration would look like. The
only line that appears relevant from running isar-help-syntax is
logic = "!(" logic[0] => "Start" (80)
Chris Capel
Email Gateway (Aug 18 2022 at 13:02):From: Chris Capel <pdf23ds@gmail.com>
Ahh, I see. You have to treat the constructor as a constant
declaration. So in my case,
no_syntax Start :: "nat => token" ("!'(_" 80)
Chris Capel
Email Gateway (Aug 18 2022 at 13:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Chris,
the easiest way to tinker around with constant syntax nowadays is the
notation / no_notation mechanism, as in the following example:
datatype foo = Bla
term Bla
notation Bla ("Blubb")
term Bla
no_notation Bla ("Blubb")
term Bla
Note that the arguments to no_notation have to match the corresponding
notation declaration exactly.
For more refer to the Isabelle Reference Manual.
Hope this helps
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC