diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-10-12 20:16:45 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-10-12 20:16:45 -0400 |
| commit | 6726ebe2e413b1f135dc968734e902cc12254126 (patch) | |
| tree | b04350f2a2d273e1d406ec80fe2fb33761e6b997 /src/Util/NatUtil.v | |
| parent | cf24ef77eeab8255e4b8465191605db145b4b1ec (diff) | |
integrate bitwise operations
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 21002dad5..ea9a5653e 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -305,3 +305,6 @@ Hint Rewrite min_idempotent_S_l : natsimplify. Lemma min_idempotent_S_r x : min x (S x) = x. Proof. omega *. Qed. Hint Rewrite min_idempotent_S_r : natsimplify. + +Lemma setbit_high : forall x i, (x < 2^i -> setbit x i = x + 2^i)%nat. +Admitted.
\ No newline at end of file |