Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Precedence of notation


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC