diff options
Diffstat (limited to 'unit-tests/Tests_verit_tactics.v')
| -rw-r--r-- | unit-tests/Tests_verit_tactics.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 6f0cb7e..896c1bf 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -976,3 +976,21 @@ Qed. (* The tactic simpl does too much here : *) (* Goal forall x, 3 + x = x + 3. *) (* nat_convert. *) + + +(* Issue 10 + https://github.com/smtcoq/smtcoq/issues/10 +*) + +Goal forall (x : positive), Zpos x <=? Zpos x. +Proof using. + intros. + verit. +Qed. + + +Goal forall (x : positive) (a : Z), (Z.eqb a a) || negb (Zpos x <? Zpos x). +Proof using. + intros. + verit. +Qed. |