Set-match-free-error
Control error vs. warning when :match-free is missing
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.
