aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Value.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/Value.v')
-rw-r--r--src/verilog/Value.v8
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.