From 3cd225e3487d830d4e9782e011483824717f2262 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Nov 2018 15:47:34 -0400 Subject: Add more zrange operations --- src/Util/ZRange/Operations.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 32924e6dc..6207a9de7 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -177,4 +177,16 @@ Module ZRange. := lower r <= upper r. 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). + Notation sub := (ZRange.four_corners Z.sub). + Notation mul := (ZRange.four_corners Z.mul). + Notation div := (ZRange.four_corners_and_zero Z.div). + Notation shiftr := (ZRange.four_corners_and_zero Z.shiftr). + Notation shiftl := (ZRange.four_corners_and_zero Z.shiftl). + Notation land := land_bounds. + Notation lor := lor_bounds. End ZRange. -- cgit v1.2.3