Example:

```
From Coq Require Import ZArith.
From Coq Require Import QArith.
Check 1%Q < 3.
Check 1%Z < 3.
```

`Error: The term "1%Z" has type "Z" while it is expected to have type "Q".`

Is there a way to use the notation for both types?

You can delimit the scope to the whole expression, i.e. `Check (1 < 3)%Z.`

Thank you Alexander. This works. However, I am having trouble with this more complicated case:

```
From Coq Require Import ZArith.
From Coq Require Import QArith.
From Coq Require Import QArith.QOrderedType.
From Coq Require Import MSets.MSets.
Module SetOfℚ := Make (Q_as_OT). Import SetOfℚ.
Module SetOfℤ := Make (Z_as_OT). Import SetOfℤ.
Notation "{ x }" := (add x empty).
Check ({ 1 })%Z.
Check ({ 1 })%Q.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )).
Check ({ 1 })%Z.
Check ({ 1 })%Q.
Check ({ 1; 2 })%Z.
Check ({ 1; 2 })%Q.
```

There are several problems here:

- It seems that
`add`

from`SetOfℤ`

shadows the one from`SetOfℚ`

, consequently the notation only works for`Z`

. - After I define the notation with the ellipsis, the notation for a singleton set stops working.

My desire is to have an ergonomic way to work with sets of ℤ and ℚ simultaneously. How can I achieve that?

This is my next iteration:

```
Open Scope Q.
Module SetOfℚ := Make (Q_as_OT). Import SetOfℚ.
Notation "{ x }" := (add x empty): Q_scope.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )): Q_scope.
Close Scope Q.
Open Scope Z.
Module SetOfℤ := Make (Z_as_OT). Import SetOfℤ.
Notation "{ x }" := (add x empty): Z_scope.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )): Z_scope.
Close Scope Z.
Check {1; 2}%Z.
Check {1; 2}%Q.
```

_(Unfortunately, the notation for singletons still does not work, for reason unknown to me.)_

I suppose this is as good as it gets. I wish I could make `add`

and `empty`

polymorphic, so that this notation were also magically polymorphic, but I do not know how.

Scopes only apply to notations. For definitions you will need to qualify them. Use `Locate add.`

to see how to qualify in your context.

math-comp does provide a generic notation for rings, also, algebraic structures are formulated so setoids are not required

similarly for order and lattice structures, tho for sets of such elements, you need to use the finmap library

as done in multinomials

Last updated: Apr 14 2024 at 11:02 UTC