diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2019-04-12 15:43:55 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2019-04-12 15:43:55 +0200 |
| commit | c2f860da64b15ef094d2905330e74658934f9cc2 (patch) | |
| tree | 7da4c0c03e4d8af1442dd51d7ef9fa2bedbe53b9 /README.md | |
| parent | d9fbf311cf6649f787a23903dc48a118b668deec (diff) | |
| download | smtcoq-c2f860da64b15ef094d2905330e74658934f9cc2.tar.gz smtcoq-c2f860da64b15ef094d2905330e74658934f9cc2.zip | |
Documentation
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -165,11 +165,12 @@ The `verit_bool [h1 ...]` tactic can be used to solve any goal of the form: forall l, b1 = b2 ``` where `l` is a quantifier-free list of terms and `b1` and `b2` are -expressions of type `bool`. This tactic *supports quantifiers*: it takes +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. These lemmas can also be given once and for all using the `Add_lemmas` command (see -examples/Example.v for details). +[examples/Example.v](https://github.com/smtcoq/smtcoq/blob/master/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 @@ -239,7 +240,7 @@ The `cvc4_bool` tactic can be used to solve any goal of the form: 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`. In addition, the `cvc4` tactic applies to Coq goals of sort `Prop`: it |