diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-09 17:37:55 -0400 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2016-10-10 13:10:32 -0400 |
| commit | 9f7ff19fe178823bf94ec532fbdf4e9fa2bfcfa6 (patch) | |
| tree | 5b83ba392e5a457d9c781ca477fa082025463ce9 /src/Util/ZUtil.v | |
| parent | 405f5840e5d9097b034a05d5eeab5ae6ba5757a3 (diff) | |
Fix compatibility with sigT notation
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c9270e9dd..d82896641 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -13,7 +13,7 @@ Local Open Scope Z. Infix ">>" := Z.shiftr : Z_scope. Infix "<<" := Z.shiftl : Z_scope. -Infix "&" := Z.land : Z_scope. +Infix "&'" := Z.land : Z_scope. Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. @@ -230,7 +230,7 @@ Ltac canonicalize_comm_step mul ls comm comm3 := Ltac canonicalize_comm mul ls comm comm3 := repeat canonicalize_comm_step mul ls comm comm3. Module Z. - Definition pow2_mod n i := (n & (Z.ones i)). + Definition pow2_mod n i := (n &' (Z.ones i)). Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b). Proof. @@ -337,7 +337,7 @@ Module Z. Qed. Hint Resolve pow2_mod_pos_bound : zarith. - Lemma land_same_r : forall a b, (a & b) & b = a & b. + Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. Proof. intros; apply Z.bits_inj'; intros. rewrite !Z.land_spec. |