diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 10:46:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-13 10:46:17 -0400 |
| commit | 4ecdd6ca43af688e5cd36ec9ab2496c4e192477d (patch) | |
| tree | e67cd24bf8cd7de2dee68253a5a6db3b5f567241 /src/Util/ZUtil/Hints/Ztestbit.v | |
| parent | facfba480b7ce797ecf70e9d128d0392d1250360 (diff) | |
Split off ZUtil initial hint databases
Diffstat (limited to 'src/Util/ZUtil/Hints/Ztestbit.v')
| -rw-r--r-- | src/Util/ZUtil/Hints/Ztestbit.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Hints/Ztestbit.v b/src/Util/ZUtil/Hints/Ztestbit.v new file mode 100644 index 000000000..d93da3ee7 --- /dev/null +++ b/src/Util/ZUtil/Hints/Ztestbit.v @@ -0,0 +1,11 @@ +Require Import Coq.ZArith.ZArith. +Require Export Crypto.Util.ZUtil.Hints.Core. + +Hint Rewrite <- Z.shiftr_div_pow2 Z.shiftr_mul_pow2 Z.shiftl_mul_pow2 Z.shiftl_div_pow2 using zutil_arith : convert_to_Ztestbit. + +Hint Rewrite Z.testbit_0_l Z.land_spec Z.lor_spec : Ztestbit. +Hint Rewrite Z.testbit_0_l Z.land_spec Z.lor_spec : Ztestbit_full. +Hint Rewrite Z.shiftl_spec Z.shiftr_spec using zutil_arith : Ztestbit. +Hint Rewrite Z.testbit_neg_r using zutil_arith : Ztestbit. +Hint Rewrite Bool.andb_true_r Bool.andb_false_r Bool.orb_true_r Bool.orb_false_r + Bool.andb_true_l Bool.andb_false_l Bool.orb_true_l Bool.orb_false_l : Ztestbit. |