Witness
Computed hint for calling the witness-cp clause processor.
Usage:
(witness :ruleset (rule ruleset ...)
:examples ((inst-rulename1 term1 term2 ...)
(inst-rulename2 term3 ...) ...)
:generalize t)
Calls the clause processor witness-cp. If a ruleset is provided,
only those witness-cp rules will be available; otherwise, all rules that are
currently enabled (see witness-enable and witness-disable) are
used.
The :generalize argument is T by default; if set to NIL, the
generalization step is skipped; see witness-cp.
The :examples argument is empty by default. Usually, examples are
generated by defexample rules. However, in some cases you might like to
instantiate universally quantified hyps in a particular way on a one-off basis;
this may be done using the :examples field. Within an example:
- Each inst-rulename must be the name of a definstantiate rule,
and
- The terms following it correspond to that rule's :vars. In
particular, the list of terms must be the same length as the :vars of the
rule.
