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, 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, and 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.