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