diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-06 13:53:33 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-06 13:53:33 -0700 |
| commit | 6ddfe39affef2f47836b03d49fc6e4b9266e75c8 (patch) | |
| tree | 429e322586e5f66dd53ef939e13c6bab0fcf5237 /src/Util | |
| parent | be1f55f6fc260aa42305b40f3853c56883d34550 (diff) | |
Add notations for Z.shift{r,l} to ZUtil
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ZUtil.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 24bf31b29..7b57afb53 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,10 +1,14 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Notations. Require Import Coq.Lists.List. Import Nat. Local Open Scope Z. +Infix ">>" := Z.shiftr : Z_scope. +Infix "<<" := Z.shiftl : Z_scope. + Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. Hint Extern 1 => nia : nia. |