Skip to content

Commit a5340b4

Browse files
committed
copilot-theorem: Remove section about combining provers in README. Refs #452.
Currently only the Kind2 prover can be combined with itself, so it no longer makes sense to have a section about combining provers. This commit removes that section.
1 parent 383f9bd commit a5340b4

File tree

1 file changed

+0
-19
lines changed

1 file changed

+0
-19
lines changed

copilot-theorem/README.md

Lines changed: 0 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -98,25 +98,6 @@ and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is
9898
equivalent to the `maxK` option of the K-Induction prover. Its default value is
9999
0, which stands for infinity.
100100

101-
#### Combining provers
102-
103-
The `combine :: Prover -> Prover -> Prover` function lets you merge two provers
104-
A and B into a prover C which launches both A and B and returns the *most
105-
precise* output. It would be interesting to implement other merging behaviours
106-
in the future. For instance, a *lazy* one such that C launches B only if A has
107-
returns *unknown* or *error*.
108-
109-
As an example:
110-
111-
```haskell
112-
prover =
113-
kInduction def {kTimeout = 5}
114-
`combine` kind2Prover def
115-
```
116-
117-
We will discuss the internals and the experimental results of these provers
118-
later.
119-
120101
### Proof schemes
121102

122103
Let's consider again this example:

0 commit comments

Comments
 (0)