diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-20 00:31:10 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-20 00:31:10 +0100 |
| commit | 2d10f818ff05b028ab2930d3ccfddd5a11bb1ad0 (patch) | |
| tree | ef1d019119386d64a553c93a88391823836f3732 /src/verilog/Value.v | |
| parent | 9215c5c6ec3312a44a0808481d03210baa859beb (diff) | |
| parent | d216c3b6dfbd80f49296b47ba46d18603c723804 (diff) | |
| download | vericert-2d10f818ff05b028ab2930d3ccfddd5a11bb1ad0.tar.gz vericert-2d10f818ff05b028ab2930d3ccfddd5a11bb1ad0.zip | |
Merge remote-tracking branch 'james/arrays-proof' into develop
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 -> |