Skip to content

Compatibility with Rocq 9.2 #21

Description

@JasonGross

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

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions