diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 17:53:54 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 17:53:54 +0100 |
| commit | 3ec28d050aebc305c6df5b4b95bcf91498ff11cc (patch) | |
| tree | a44487a90e334a22550a2e64c26d59329daf1170 /src | |
| parent | 9491b9dda35897c8abde560b79a323d47aac0ec4 (diff) | |
| download | vericert-3ec28d050aebc305c6df5b4b95bcf91498ff11cc.tar.gz vericert-3ec28d050aebc305c6df5b4b95bcf91498ff11cc.zip | |
Admit the value proof
Diffstat (limited to 'src')
| -rw-r--r-- | src/verilog/Value.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index ad946ca..253595b 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -381,6 +381,8 @@ Proof. - rewrite wzero'_def. apply wordToNat_wzero. - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. auto. inversion H. destruct (2 ^ Z.of_nat sz)%Z eqn:?; try discriminate. - Set Printing All. - Search positive Z. - - lia. +(* Set Printing All. + Search positive Z.*) + admit. + - admit. +Admitted. |