From 6726ebe2e413b1f135dc968734e902cc12254126 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 12 Oct 2016 20:16:45 -0400 Subject: integrate bitwise operations --- src/Util/NatUtil.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Util/NatUtil.v') 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 -- cgit v1.2.3