make reversed list notations left-associative

mit-plv · Apr 18, 2024 · 53e60da · 53e60da
1 parent e059c0d
commit 53e60da
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/bedrock2/src/bedrock2/ReversedListNotations.v b/bedrock2/src/bedrock2/ReversedListNotations.v
@@ -1,4 +1,6 @@
 Require Coq.Lists.List.
 
-Notation "xs ;+ x" := (cons x xs) (at level 60, format "xs ;+ x") : list_scope.
-Notation "xs ;++ ys" := (app ys xs) (at level 60, format "xs  ;++  ys") : list_scope.
+Notation "xs ;+ x" := (cons x xs)
+  (at level 59, format "xs  ;+  x", left associativity) : list_scope.
+Notation "xs ;++ ys" := (app ys xs)
+  (at level 59, format "xs  ;++  ys", left associativity) : list_scope.