From 83998e544f51f06026fb32d115b74f9d1303e629 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 22 Apr 2020 00:12:24 +0100 Subject: Remove unnecessary Lemma Still cannot run these functions inside Coq itself, however, they work when they are extracted to Caml. --- src/verilog/Value.v | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'src/verilog') 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. -- cgit