From 9e29a351fd0928130fa0b67dc47b67cdf989e4b7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 24 Jun 2020 17:53:36 +0100 Subject: Fixes to make develop compile --- src/verilog/Value.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'src/verilog') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index bde98b8..52a87e3 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -372,7 +372,7 @@ Lemma boolToValue_ValueToBool : valueToBool (boolToValue 32 b) = b. Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. -Lemma ZToValue_valueToNat : +(*Lemma ZToValue_valueToNat : forall x sz, sz > 0 -> (x < 2^(Z.of_nat sz))%Z -> @@ -384,7 +384,5 @@ Proof. unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) - Search Pos.to_nat. - (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *) - Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n). - econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat. + Search "inj" positive nat. +*) -- cgit