diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-28 16:26:11 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-28 16:26:11 +0100 |
| commit | b96d222d47da5c5d59b65dfa152e255b7a4f7b46 (patch) | |
| tree | 31535b8d1ec3c295bc96727580446297341e65d0 /examples | |
| parent | a25181f93604e279b899552b119d68df0c63b0ad (diff) | |
| download | smtcoq-b96d222d47da5c5d59b65dfa152e255b7a4f7b46.tar.gz smtcoq-b96d222d47da5c5d59b65dfa152e255b7a4f7b46.zip | |
int does not exist in standard coq
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/examples/Example.v b/examples/Example.v index b83e619..5c740d6 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -62,10 +62,7 @@ Proof. zchaff. Qed. -Goal forall i j k, - let a := (i == j)%int in - let b := (j == k)%int in - let c := (k == i)%int in +Goal forall a b c, (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. Proof. zchaff. |