From 3ec28d050aebc305c6df5b4b95bcf91498ff11cc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 17:53:54 +0100 Subject: Admit the value proof --- src/verilog/Value.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src') 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. -- cgit