diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ZRange/Operations.v | 12 |
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. |