:match-free is missing
Major Section: SWITCHES-PARAMETERS-AND-MODES
Legal Forms: (set-match-free-error nil) :set-match-free-error nil (set-match-free-error t) :set-match-free-error t
As described elsewhere (see free-variables), when a rewrite,
linear, or forward-chaining rule has free variables in its
hypotheses, the user can specify whether to try all bindings
(``:all'') or just the first (``:once'') when relieving its
hypotheses, as a basis for relieving subsequent hypotheses. This direction
of :all or :once is generally provided by specifying either
:match-free :once or :match-free :all in the :rule-classes
of the rule.
But suppose that neither of these is specified for such a rule. (Note:
set-match-free-error is not relevant for type-prescription rules.)
Also suppose that set-match-free-default has not specified a default of
:once or :all (see set-match-free-default). In this case a warning
will occur except when in the context of include-book. If you prefer
to see an error in such cases, except in the context of certify-book,
execute (set-match-free-error t). If there is no error, then a default
of :all is used.
Note: This is NOT an event! Instead, set-match-free-error sets the
state global 'match-free-error (see state and see assign). Thus, this
form cannot be put into a book. If you are tempted to put it into a book,
consider the fact that it really isn't needed there, since the absence of
:match-free does not cause an error in the context of certify-book
or include-book. If you still feel the need for such a form, consider
using set-match-free-default to provide a default, at least within the
scope of the current book (if any); see set-match-free-default.
