diff options
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 8a0716d..a96d67c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -200,6 +200,10 @@ Proof. split; intros. unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?. - destruct v1, v2. simpl in H. +Abort. + +Definition value_int_eqb (v : value) (i : int) : bool := + Z.eqb (valueToZ v) (Int.unsigned i). (** Arithmetic operations over [value], interpreting them as signed or unsigned depending on the operation. |