Gergely Buday (Aug 04 2020 at 11:14): Gergely Buday (Aug 04 2020 at 11:14):Here is my simple locale definition in Isabelle:
locale sig =
fixes le:: "'a ⇒ 'a ⇒ bool" (infixl "≤" 50)
assumes refl: "x ≤ x"
Now, I get an error message:
Ambiguous input⌂ produces 2 parse trees:
("\<^const>HOL.Trueprop"
("\<^const>Orderings.ord_class.less_eq" ("_position" x) ("_position" x)))
("\<^const>HOL.Trueprop" ("\<^fixed>le" ("_position" x) ("_position" x)))
Ambiguous input
2 terms are type correct:
(x ≤ x)
(x ≤ x)
Failed to parse prop
Do I have a conflict with a builtin less-or-equal operator?
How can I fix this?
The Coq original I took uses
Infix "≤" := le : order_scope.
Open Scope order_scope.
So, it instructs the system to use less-or-equal "≤" only in a scope. Is there similar functionality in Isabelle?
Kevin Kappelmann (Aug 04 2020 at 11:26):If you ctrl+f "notation" in Orderings.thy, you will see the defined notation for leq. You can copy the respective notation declarations and disable them using no_notation. In this case
no_notation
less_eq ("'(≤')") and
less_eq ("(_/ ≤ _)" [51, 51] 50)
Thanks, Kevin Kappelmann. Is there scoping a 'la Coq in Isabelle?
Lukas Stevens (Aug 04 2020 at 11:54):You can use locales as a scoping mechanism. However, notation outside of locales is global. It is therefore recommended to use bundles which allow you to enable/disable notation.
Kevin Kappelmann (Aug 04 2020 at 12:01):With contexts, you could do this:
bundle no_less_eq_syntax
begin
no_notation less_eq ("'(≤')") and less_eq ("(_/ ≤ _)" [51, 51] 50)
end
context
includes no_less_eq_syntax
begin
term "(≤)" ―‹does not work (as intended)›
end
term "(≤)" ―‹works›
However, with locales, it seems like you cannot use includes. So the best thing I could come up with is this:
bundle less_eq_syntax
begin
notation less_eq ("'(≤')") and less_eq ("(_/ ≤ _)" [51, 51] 50)
end
bundle no_less_eq_syntax
begin
no_notation less_eq ("'(≤')") and less_eq ("(_/ ≤ _)" [51, 51] 50)
end
unbundle no_less_eq_syntax
locale sig =
fixes le:: "'a ⇒ 'a ⇒ bool" (infixl "≤" 50)
assumes refl: "x ≤ x" ―‹works›
begin
end
unbundle less_eq_syntax
term "(≤)" ―‹works›
Last updated: Dec 21 2024 at 16:20 UTC