From fa39e09d403cfba1b1e6c359362e54600dfc28b0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 23:12:59 +0100 Subject: Use associations instead of state --- src/verilog/Value.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/verilog/Value.v') 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. -- cgit