From 9a7c314bea5ba24577e983a9f87feaf5b380bc0f Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 15 May 2020 17:20:25 +0200 Subject: Close #10 --- unit-tests/Tests_verit_tactics.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'unit-tests/Tests_verit_tactics.v') 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