Is it expected that (apparently) the standard operations on primitive integers are not bound to standard notations, even in `uint63_scope`

, as shown by:

```
Require Import PrimInt63.
Parameter x : int.
Fail Check (2+x)%uint63. (* "x" has type "int" while it is expected to have type "nat" *)
Check add 2%uint63 x. (* ok *)
```

Would there be problems at adding notations such as:

```
Notation "x + y" := (PrimInt63.add x y) : uint63_scope.
Check (2+x)%uint63. (* now ok *)
```

the notations are in Uint63 not PrimInt63

Or Sint63

Last updated: Oct 13 2024 at 01:02 UTC