diff options
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index bde98b8..becc44c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -388,3 +388,4 @@ Proof. (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *) Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n). econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat. +Admitted. |