diff options
| author | James Pollard <james@pollard.dev> | 2020-06-11 14:47:52 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-11 14:47:52 +0100 |
| commit | d0257b0a47ad998e01715e9bc6ba612b834765f1 (patch) | |
| tree | a356047d4cc1a0f6fb008d63512184d4075ee4e4 /src/verilog/Value.v | |
| parent | d3be4601c9bc68fddaf4dc08c648f03d95a39e1d (diff) | |
| download | vericert-d0257b0a47ad998e01715e9bc6ba612b834765f1.tar.gz vericert-d0257b0a47ad998e01715e9bc6ba612b834765f1.zip | |
Working on proof.
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index d527b15..b1ee353 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + Lemma valueToZ_ZToValue : forall n z, (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> |