Compatibility with Rocq 9.2 #21
Description
In Rocq 9.2, the standard library defines _ ~ 1 and _ ~ 0 notations for positive numbers at a fixed level. The local redefinition in Module Integers at a different level causes a hard error.
This works, but the printing associates the wrong way and so this is maybe not what you want
diff --git a/vfa-current/Trie.v b/vfa-current/Trie.v
index 275284d5..c05fee2a 100644
--- a/vfa-current/Trie.v
+++ b/vfa-current/Trie.v
@@ -167,12 +167,17 @@ Fixpoint print_in_binary (p: positive) : list nat :=
Eval compute in print_in_binary ten. (* = [1; 0; 1; 0] *)
(** Another way to see the "binary representation" is to make up
- postfix notation for [xI] and [xO], as follows *)
-
-Notation "p ~ 1" := (xI p)
- (at level 7, left associativity, format "p '~' '1'").
-Notation "p ~ 0" := (xO p)
- (at level 7, left associativity, format "p '~' '0'").
+ postfix notation for [xI] and [xO]. As of Rocq 9.2, the standard
+ library already defines [_ ~ 1] and [_ ~ 0] at a fixed level, so
+ to avoid a conflict we use a custom scope bound to our local
+ [positive] type. *)
+
+Declare Scope mypos_scope.
+Delimit Scope mypos_scope with mypos.
+Bind Scope mypos_scope with positive.
+Notation "p ~ 1" := (xI p) : mypos_scope.
+Notation "p ~ 0" := (xO p) : mypos_scope.
+Open Scope mypos_scope.
Print ten. (* = xH~0~1~0 : positive *)