SET-MATCH-FREE-ERROR

Major Section:  EVENTS

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 or linear rule has free variables in its hypotheses, the user generally specifies 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, and that set-match-free-default has not specified a default of :once or :all (see set-match-free-default). In this case an error will occur except when in the context of certify-book or include-book. The error can be replaced with a warning for all future such rules, by executing (set-match-free-error nil). If indeed there is no error (because this form has been executed or because a certify-book or include-book is in progress), 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.