diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 15:39:35 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-27 15:39:35 +0200 |
| commit | 0334ceccaf14716d81db8a73f7d414d33b91cd8b (patch) | |
| tree | 9880cfed3e65f2cc6eb7c063ee52c339f0412ed7 /examples | |
| parent | db9bb4f7ba88c938e882f9a30c6456d73b793491 (diff) | |
| download | smtcoq-0334ceccaf14716d81db8a73f7d414d33b91cd8b.tar.gz smtcoq-0334ceccaf14716d81db8a73f7d414d33b91cd8b.zip | |
Zeq_bool -> Z.eqb
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/examples/Example.v b/examples/Example.v index 2f3ca73..fe00931 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -53,7 +53,7 @@ Qed. Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), - (negb (Zeq_bool (f a) b)) || (negb (P (f a))) || (P b). + negb (f a =? b) || negb (P (f a)) || (P b). Proof. verit. Qed. @@ -62,9 +62,9 @@ Qed. Goal forall b1 b2 x1 x2, implb (ifb b1 - (ifb b2 (Zeq_bool (2*x1+1) (2*x2+1)) (Zeq_bool (2*x1+1) (2*x2))) - (ifb b2 (Zeq_bool (2*x1) (2*x2+1)) (Zeq_bool (2*x1) (2*x2)))) - ((implb b1 b2) && (implb b2 b1) && (Zeq_bool x1 x2)). + (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) + (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) + ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). Proof. verit. Qed. |