diff options
Diffstat (limited to 'src/Util/ZRange.v')
| -rw-r--r-- | src/Util/ZRange.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index 4f1e4f806..8badcb492 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -68,6 +68,9 @@ Proof. split; intro H; (repeat let x := fresh in intro x; specialize (H x)); omega. Qed. +Definition is_bounded_by_bool (v : Z) (x : zrange) : bool + := ((lower x <=? v) && (v <=? upper x))%bool%Z. + Definition is_tighter_than_bool (x y : zrange) : bool := ((lower y <=? lower x) && (upper x <=? upper y))%bool%Z. |