diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 17:53:36 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-24 17:53:36 +0100 |
| commit | 9e29a351fd0928130fa0b67dc47b67cdf989e4b7 (patch) | |
| tree | 4da1b4e4a40c1b5905c5d0d08342bf9e839db6d9 /src/verilog | |
| parent | e60d6c39dd960da14383a823a382e55f88258588 (diff) | |
| download | vericert-9e29a351fd0928130fa0b67dc47b67cdf989e4b7.tar.gz vericert-9e29a351fd0928130fa0b67dc47b67cdf989e4b7.zip | |
Fixes to make develop compile
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. +*) |