diff options
author | XZ-X <x1456776728@icloud.com> | 2021-01-05 16:48:19 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-05 09:48:19 +0100 |
commit | 73c49626476ed7ae4313f92431a9dea0b4eeb51d (patch) | |
tree | 9555c19ef43e009e0362f8d1fe65f6207a778547 /USE.md | |
parent | 3d11e77273cfb6e10758ad242035e106f502fda8 (diff) | |
download | smtcoq-73c49626476ed7ae4313f92431a9dea0b4eeb51d.tar.gz smtcoq-73c49626476ed7ae4313f92431a9dea0b4eeb51d.zip |
Change imports from `SMTCoq` to `SMTCoq.SMTCoq` (#83)
* Update USE.md and `README.md`
Change the imports in `USE.md` and `README.md` from `SMTCoq` to `SMTCoq.SMTCoq`
Diffstat (limited to 'USE.md')
-rw-r--r-- | USE.md | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -14,7 +14,7 @@ easily re-usable for your own usage. ## Overview After installation, the SMTCoq module can be used in Coq files via the -`Require Import SMTCoq.` command. For each supported solver, it +`Require Import SMTCoq.SMTCoq.` command. For each supported solver, it provides: - a vernacular command to check answers: `XXX_Checker "problem_file" @@ -60,7 +60,7 @@ To check the result given by zChaff on an unsatisfiable dimacs file - In a Coq file `file.v`, put: ```coq -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Zchaff_Checker "file.cnf" "resolve_trace". ``` @@ -70,7 +70,7 @@ Zchaff_Checker "file.cnf" "resolve_trace". - You can also produce Coq theorems from zChaff proof witnesses: the commands ```coq -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Zchaff_Theorem theo "file.cnf" "resolve_trace". ``` will produce a Coq term `theo` whose type is the theorem stated in @@ -111,7 +111,7 @@ This command produces a proof witness file named `file.log`. - In a Coq file `file.v`, put: ```coq -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Section File. Verit_Checker "file.smt2" "file.log". End File. @@ -123,7 +123,7 @@ End File. - You can also produce Coq theorems from veriT proof witnesses: the commands ```coq -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Section File. Verit_Theorem theo "file.smt2" "file.log". End File. @@ -186,7 +186,7 @@ This set of commands produces a proof witness file named `name.lfsc`. - In a Coq file `name.v`, put: ```coq -Require Import SMTCoq Bool List. +Require Import SMTCoq.SMTCoq Bool List. Import ListNotations BVList.BITVECTOR_LIST FArray. Local Open Scope list_scope. Local Open Scope farray_scope. |