diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-09 20:35:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-09 20:35:11 -0400 |
| commit | 5c027fc4da43d3ad1398451ba4352d1d11607815 (patch) | |
| tree | c42f6b39076bc473aade1cdf9739cf60359c9d15 /src/Util/ZUtil.v | |
| parent | ca5402e5c10d5283869229c2765349a553033a98 (diff) | |
Add more to Ztestbit_full
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c98b63554..a5e87b92c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -855,6 +855,7 @@ Module Z. repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega. Qed. Hint Rewrite shiftl_spec_full : Ztestbit. + Hint Rewrite shiftl_spec_full : Ztestbit_full. Lemma shiftr_spec_full a n m : Z.testbit (a << n) m = if Z_lt_dec m n @@ -866,6 +867,7 @@ Module Z. repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega. Qed. Hint Rewrite shiftl_spec_full : Ztestbit. + Hint Rewrite shiftl_spec_full : Ztestbit_full. (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *) Ltac zero_bounds' := |