Email Gateway (Aug 18 2022 at 09:34): Email Gateway (Aug 18 2022 at 09:34):From: Christian Sternagel <Christian.Sternagel@uibk.ac.at>
As far as I figured out, it is not possible to
define a translation like
syntax
"_common_rewrite_step" :: "['a, 'a, 'a] => bool" ("_ ---> _ <--- _" 100)
translations
"a ---> c <--- b" == "(a,c) : r & (b,c) : r"
because internally two rewrite rules are established and
one of it is not left-linear.
Is there another way to define abbreviations like above?
mfG
Christian Sternagel
Email Gateway (Aug 18 2022 at 09:35):From: Makarius <makarius@sketis.net>
On Wed, 30 Aug 2006, Christian Sternagel wrote:
As far as I figured out, it is not possible to define a translation like
translations
"a ---> c <--- b" == "(a,c) : r & (b,c) : r"
because internally two rewrite rules are established and one of it is
not left-linear.
You can omit the second one by using => instead of == above. This will at
least provide the input syntax. The other direction can be done by
low-level ML translations (cf. parse_translation), although I do not
recommend this.
Is there another way to define abbreviations like above?
In future versions of Isabelle, using 'abbreviation'.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC