diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-07 23:12:59 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-07 23:12:59 +0100 |
| commit | fa39e09d403cfba1b1e6c359362e54600dfc28b0 (patch) | |
| tree | 72611b65df13987577afde0d572469d49361083f /src/verilog/Value.v | |
| parent | c8535e1f454c7014c7b794fc8be343e2fda97937 (diff) | |
| download | vericert-fa39e09d403cfba1b1e6c359362e54600dfc28b0.tar.gz vericert-fa39e09d403cfba1b1e6c359362e54600dfc28b0.zip | |
Use associations instead of state
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. |