From 82c316e4f6d44c0b6f8f7142dc0413c8d7b0eeab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Mar 2017 19:15:10 -0400 Subject: Add is_tighter_than_bool to zrange --- src/Util/ZRange.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/ZRange.v') diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index 7b9329dca..fab098037 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -37,6 +37,9 @@ Section with_bitwidth. := Tuple.pointwise2 is_bounded_by'. End with_bitwidth. +Definition is_tighter_than_bool (x y : zrange) : bool + := ((lower y <=? lower x) && (upper x <=? upper y))%bool%Z. + Global Instance dec_eq_zrange : DecidableRel (@eq zrange) | 10. Proof. intros [lx ux] [ly uy]. @@ -49,4 +52,5 @@ Module Export Notations. Delimit Scope zrange_scope with zrange. Notation "r[ l ~> u ]" := {| lower := l ; upper := u |} (format "r[ l ~> u ]") : zrange_scope. + Infix "<=?" := is_tighter_than_bool : zrange_scope. End Notations. -- cgit v1.2.3