From 8dd2ff5ebfd6dd49da64e4707f98f55bf76e36a8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Nov 2018 16:06:08 -0400 Subject: Add zrange notations --- src/Util/ZRange/Operations.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'src/Util') 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. -- cgit v1.2.3