diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 17:43:40 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 17:43:40 +0100 |
| commit | 44a7c303c34dabd68e8d28c7de6ee54cc03a774b (patch) | |
| tree | a9ba244d6964a851865ba2f672ae9fab8aadb3a3 | |
| parent | ff8c032211641b3d0b6482ce0dadc87e957ccb0d (diff) | |
| download | smtcoq-44a7c303c34dabd68e8d28c7de6ee54cc03a774b.tar.gz smtcoq-44a7c303c34dabd68e8d28c7de6ee54cc03a774b.zip | |
Unit test for double negation
| -rw-r--r-- | unit-tests/Tests.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/unit-tests/Tests.v b/unit-tests/Tests.v index d011cdb..3b8d95a 100644 --- a/unit-tests/Tests.v +++ b/unit-tests/Tests.v @@ -65,6 +65,10 @@ Goal forall a, negb (a || negb a) = false. zchaff. Qed. +Goal forall a, negb (negb (a || negb a)). + zchaff. +Qed. + Goal forall a, (a && negb a) = false. zchaff. Qed. |