diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-31 19:15:10 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-31 19:15:10 -0400 |
| commit | 82c316e4f6d44c0b6f8f7142dc0413c8d7b0eeab (patch) | |
| tree | eb1ed0cf3a6f91a934f87fde4c0a24d3d6b860cd /src/Util/ZRange.v | |
| parent | 5f7281089fd0a101acb365cfcd432a06b7bfe680 (diff) | |
Add is_tighter_than_bool to zrange
Diffstat (limited to 'src/Util/ZRange.v')
| -rw-r--r-- | src/Util/ZRange.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |