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?

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?

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.

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: Aug 10 2022 at 19:17 UTC