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 | |
parent | 93bd71388291d2e526a30c56e7fe63744f98e64d (diff) | |
download | smtcoq-d9fbf311cf6649f787a23903dc48a118b668deec.tar.gz smtcoq-d9fbf311cf6649f787a23903dc48a118b668deec.zip |
Documentation
-rw-r--r-- | INSTALL.md | 6 | ||||
-rw-r--r-- | README.md | 8 |
2 files changed, 10 insertions, 4 deletions
@@ -249,7 +249,7 @@ The `zchaff` binary must be present in your PATH to use it through SMTCoq. ## Setting up environment for SMTCoq ### Using SMTCoq without installing -If you want to use SMTCoq without installing it your Coq installation, you can +If you want to use SMTCoq without adding it to your Coq installation, you can tell Coq where to find SMTCoq by adding the following line in the file `~/.config/coqrc`: @@ -257,6 +257,10 @@ tell Coq where to find SMTCoq by adding the following line in the file Add Rec LoadPath "~/path/to/smtcoq/src" as SMTCoq. ``` +See [this +documentation](https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-resource-file) +if it does not work. + ### Emacs and ProofGeneral @@ -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 |