From f6733c0048eacc911feff5277fed12fb544c7299 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 25 Feb 2016 13:46:07 -0500 Subject: Factor out some bedrock dependencies into WordUtil Also move a definition about words, with a TODO about location, into WordUtil. --- src/Util/NatUtil.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src/Util/NatUtil.v') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 256654df7..4ba6d0808 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,5 +1,4 @@ Require Import NPeano Omega. -Require Import Bedrock.Word. Local Open Scope nat_scope. @@ -57,8 +56,3 @@ Proof. rewrite <- nat_compare_lt; auto. } Qed. - -Lemma pow2_id : forall n, pow2 n = 2 ^ n. -Proof. - induction n; intros; simpl; auto. -Qed. -- cgit v1.2.3