From c2f860da64b15ef094d2905330e74658934f9cc2 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 12 Apr 2019 15:43:55 +0200 Subject: Documentation --- README.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index d91a9a6..56af044 100644 --- a/README.md +++ b/README.md @@ -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 -- cgit