diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-04-22 00:12:24 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-22 00:12:24 +0100 |
| commit | 83998e544f51f06026fb32d115b74f9d1303e629 (patch) | |
| tree | 74b223dced6129af2e6943c310a73201ef9391e0 | |
| parent | 5e440ccec06e740c0ee8dc8eb0e54a7284d5aef7 (diff) | |
| download | vericert-83998e544f51f06026fb32d115b74f9d1303e629.tar.gz vericert-83998e544f51f06026fb32d115b74f9d1303e629.zip | |
Remove unnecessary Lemma
Still cannot run these functions inside Coq itself, however, they work
when they are extracted to Caml.
| -rw-r--r-- | src/verilog/Value.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index be6babf..fe53dbc 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -102,14 +102,6 @@ Proof. right; trivial. Defined. -Definition value_eq_size_nat: - forall (sz : nat) (v : value), { sz = vsize v } + { True }. -Proof. - intros; destruct (Nat.eqb sz (vsize v)) eqn:?. - left; apply Nat.eqb_eq in Heqb; assumption. - right; trivial. -Defined. - Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) (EQ : vsize v1 = vsize v2) : A := let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in @@ -153,6 +145,7 @@ be called over [Z] explicitly, which is where the bits are interpreted in a signed manner. *) Definition vplus v1 v2 := map_word2 wplus v1 v2. +Definition vplus_opt v1 v2 := map_word2_opt wplus v1 v2. Definition vminus v1 v2 := map_word2 wminus v1 v2. Definition vmul v1 v2 := map_word2 wmult v1 v2. Definition vdiv v1 v2 := map_word2 wdiv v1 v2. |