Email Gateway (Aug 22 2022 at 21:06): Email Gateway (Aug 22 2022 at 21:06):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Say I have defined a ternary relation R :: A ⇒ B ⇒ A ⇒ bool with
mixfix syntax _ →⟨_⟩ _. Now I want to define an alternative notation
that allows me to fix the second argument. I use the following
declaration:
abbreviation R' :: "B ⇒ A ⇒ A ⇒ bool" (‹'(→⟨_⟩')›) where
"(→⟨u⟩) x y ≡ x →⟨u⟩ y"
Sadly the abbreviation R' takes precedence over R when printing; so
for example
term "x →⟨u⟩ y"
yields the output (→⟨u⟩) x y. How can I make sure that the notation
for R' is only used when there are less than three arguments?
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:19):From: Makarius <makarius@sketis.net>
You probably want to use "(input)" for the abbreviation (see isar-ref manual):
abbreviation (input) R' :: "'b ⇒ 'a ⇒ 'a ⇒ bool" (‹'(→⟨_⟩')›)
where "(→⟨u⟩) x y ≡ x →⟨u⟩ y"
Makarius
Last updated: Nov 21 2024 at 12:39 UTC