diff options
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/Value.v | 8 |
1 files changed, 3 insertions, 5 deletions
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. +*) |