diff options
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 |