diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 00:38:19 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-05 00:38:26 +0100 |
| commit | 5d4aed9030565349a83f9ede4bd35c020eb416b5 (patch) | |
| tree | 57f284d6277ebfdf8294dc8737075ab08c48a69a /src/verilog/Value.v | |
| parent | 2df5dc835efa3ac7552363e81ef9af5d3145cc7e (diff) | |
| download | vericert-kvx-5d4aed9030565349a83f9ede4bd35c020eb416b5.tar.gz vericert-kvx-5d4aed9030565349a83f9ede4bd35c020eb416b5.zip | |
Simplifications to proof
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 39d1832..61f2652 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -101,8 +101,6 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) -Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined. - Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. intros; subst; assumption. Defined. |