diff options
| author | James Pollard <james@pollard.dev> | 2020-06-03 19:38:40 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-03 19:38:40 +0100 |
| commit | 0729bb6e93307567cc21702005ea1d8c8dddaf8f (patch) | |
| tree | 552a10d138056ff26403dc3b72af6c32e27b55c6 /src/verilog | |
| parent | e3c66ff88570c5370b37f51404f71f485d2e5dfe (diff) | |
| parent | 971b35fd4af24cfffc462df13f8c5b9be982858e (diff) | |
| download | vericert-0729bb6e93307567cc21702005ea1d8c8dddaf8f.tar.gz vericert-0729bb6e93307567cc21702005ea1d8c8dddaf8f.zip | |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/verilog')
| -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 efbd99c..d527b15 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -356,3 +356,8 @@ Proof. unfold valToValue in H. inversion H. symmetry. apply valueToInt_intToValue. Qed. + +Lemma boolToValue_ValueToBool : + forall b, + valueToBool (boolToValue 32 b) = b. +Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. |