|
|
|---|
|
|
|
|---|
Name a set of witness-cp rules.
The witness computed-hint macro takes a
Usage:
(def-witness-ruleset foo-rules '(foo-instancing foo-witnessing bar-example-for-foo baz-example-for-foo))
After submitting this form, the following invocations of WITNESS are equivalent:
(witness :ruleset foo-rules) (witness :ruleset (foo-rules)) (witness :ruleset (foo-instancing foo-witnessing bar-example-for-foo baz-example-for-foo))
These rulesets are defined using a table event. If multiple different definitions are given for the same ruleset name, the latest one is always in effect.
Rulesets can contain other rulesets. These are expanded at the time the witness hint is run. A ruleset can be expanded with
(witness-expand-ruleset names (w state))
Witness rules can also be enabled/disabled using witness-enable and witness-disable; these settings take effect when WITNESS is called without specifying a ruleset. Ruleset names may be used in witness-enable and witness-disable just as they are used in the ruleset argument of WITNESS.