diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-26 15:10:24 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-06-26 15:10:24 -0400 |
| commit | 78656baa06ed1daeb7ba90c2d429228516dc8475 (patch) | |
| tree | dd8423b57e107e8fb2efcb2d22438edc723845f4 /src/Util/ZRange.v | |
| parent | 19fd81bfae1d8fad0b31a8415e4259c11ab80c0a (diff) | |
Add a couple of zrange lemmas
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. |