Add zrange notations

1 files changed, 11 insertions, 1 deletions

diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 6207a9de7..1497cb1ab 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -178,7 +178,6 @@ Module ZRange.
   Definition goodb (r : zrange) : bool
     := (lower r <=? upper r)%Z.
 
-  Notation opp := (ZRange.two_corners Z.opp).
   Notation log2 := (ZRange.two_corners Z.log2).
   Notation log2_up := (ZRange.two_corners Z.log2_up).
   Notation add := (ZRange.four_corners Z.add).
@@ -189,4 +188,15 @@ Module ZRange.
   Notation shiftl := (ZRange.four_corners_and_zero Z.shiftl).
   Notation land := land_bounds.
   Notation lor := lor_bounds.
+
+  Module ZRangeNotations.
+    Notation "- x" := (opp x) : zrange_scope.
+    Infix "+" := add : zrange_scope.
+    Infix "-" := sub : zrange_scope.
+    Infix "*" := mul : zrange_scope.
+    Infix "/" := div : zrange_scope.
+    Infix ">>" := shiftr : zrange_scope.
+    Infix "<<" := shiftl : zrange_scope.
+    Infix "&'" := land : zrange_scope.
+  End ZRangeNotations.
 End ZRange.