Stream: Coq devs & plugin devs

Topic: Notations for primitive int63


view this post on Zulip Hugo Herbelin (Oct 28 2023 at 09:28):

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 *)

view this post on Zulip Gaëtan Gilbert (Oct 28 2023 at 09:36):

the notations are in Uint63 not PrimInt63

view this post on Zulip Pierre Roux (Oct 28 2023 at 09:43):

Or Sint63


Last updated: Oct 13 2024 at 01:02 UTC