diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-04-12 15:40:55 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-04-12 15:40:55 +0200 |
| commit | d9fbf311cf6649f787a23903dc48a118b668deec (patch) | |
| tree | f5534eb45e23ebe86328358001c4e068c92683d7 /README.md | |
| parent | 93bd71388291d2e526a30c56e7fe63744f98e64d (diff) | |
| download | smtcoq-d9fbf311cf6649f787a23903dc48a118b668deec.tar.gz smtcoq-d9fbf311cf6649f787a23903dc48a118b668deec.zip | |
Documentation
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -105,7 +105,7 @@ The `zchaff` tactic can be used to solve any goal of the form: ```coq forall l, b1 = b2 ``` -where `l` is a quantifier-free list of variables and `b1` and `b2` are +where `l` is a quantifier-free list of terms and `b1` and `b2` are expressions of type `bool`. A more efficient version of this tactic, called `zchaff_no_check`, @@ -164,10 +164,12 @@ The `verit_bool [h1 ...]` tactic can be used to solve any goal of the form: ```coq forall l, b1 = b2 ``` -where `l` is a quantifier-free list of variables and `b1` and `b2` are +where `l` is a quantifier-free list of terms and `b1` and `b2` are expressions of type `bool`. This tactic *supports quantifiers*: it takes optional arguments which are names of universally quantified -lemmas/hypotheses that can be used to solve the goal. +lemmas/hypotheses that can be used to solve the goal. These lemmas can +also be given once and for all using the `Add_lemmas` command (see +examples/Example.v for details). In addition, the `verit` tactic applies to Coq goals of sort `Prop`: it first converts the goal into a term of type `bool` (thanks to the |