Email Gateway (Aug 22 2022 at 15:52): Email Gateway (Aug 22 2022 at 15:52):From: Diego Marmsoler <diego.marmsoler@tum.de>
Dear Isabelle experts,
I have the following problem when trying to build a locale and changing the concrete syntax of a binder:
Let’s say I have the following definition within locale A:
definition myBinder :: "('a ⇒ bool) ⇒ bool" (binder "Ab" 10)
where "myBinder P ≡ True"
Now lets say I have another locale B which is based on A and for which I want to change the syntax of myBinder.
Therefore I add the following in B:
notation myBinder (binder "Bb" 10)
now I get the following error message: “More than one parse translation for "\<^const>MyTheory.A.myBinder_binder”
Does someone know how to change the syntax of a binder within a locale?
(By the way it works well for any other mixfix notation)
Many thanks,
Diego
smime.p7s
Email Gateway (Aug 22 2022 at 15:52):From: Diego Marmsoler <diego.marmsoler@tum.de>
It seems that the behavior can be reproduced even without a hierarchy of locales.
The following reproduces the error message:
locale A
begin
definition test:: "('a ⇒ bool) ⇒ bool" (binder "+" 10)
where "test P ≡ True"
notation test (binder "-" 10)
end
without locale it doesn't produce any error message.
Best,
Diego
smime.p7s
Email Gateway (Aug 22 2022 at 15:53):From: Makarius <makarius@sketis.net>
The binder notation consists of some special tricks on top of syntax
translations. The example above shows that local changes of binder
syntax has never been used before. Such corner cases may or may not work
and it is apriori unclear if that is strange or normal. Isabelle is so
complex that it is possible to fall off the "inhabitable area" occasionally.
Anyway, a quick test shows that it is possible to remove the old binder
explicitly with 'no_notation' and then add the new one, e.g. like this:
context
begin
definition test:: "('a ⇒ bool) ⇒ bool"
where "test P ≡ True"
notation test (binder "+" 10)
no_notation test (binder "+" 10)
notation test (binder "-" 10)
end
A few more notes:
* Definitions in Isabelle/HOL are usually expressed with the equality
of HOL (=), not the one of Pure (≡). The latter is used internally for
foundational purposes, although some users have the habit to abuse it
for HOL definitions, because they like the syntactic priority better.
Note that for expressions of type bool, it is also possible to use the
notation ⟷ which has lower syntactic priority (but for binders
parentheses are required nonetheless).
* Camel case is normally not used in Isabelle sources: there is a
general quest for readability of specifications and proofs and
camelCaseIsSimplyNotReadable.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC