Stream: Beginner Questions

Topic: Ambigous parsing


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

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

view this post on Zulip Gergely Buday (Aug 04 2020 at 11:30):

Thanks, Kevin Kappelmann. Is there scoping a 'la Coq in Isabelle?

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

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC