diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-05-15 17:20:25 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-05-15 17:20:25 +0200 |
| commit | 9a7c314bea5ba24577e983a9f87feaf5b380bc0f (patch) | |
| tree | f303c626f64f33f0b4770cae6d4b03d5f4970819 /unit-tests | |
| parent | de0d13cb837223cac63f848649f39468e453ec78 (diff) | |
| download | smtcoq-9a7c314bea5ba24577e983a9f87feaf5b380bc0f.tar.gz smtcoq-9a7c314bea5ba24577e983a9f87feaf5b380bc0f.zip | |
Close #10
Diffstat (limited to 'unit-tests')
| -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. |