Set-match-free-default
Provide default for :match-free in future rules
General Forms:
(set-match-free-default :once)
(set-match-free-default :all)
(set-match-free-default nil)
Note: This utility does not apply to type-prescription rules; for a
related topic pertinent to such rules, see free-variables-type-prescription.
As described elsewhere (see free-variables), a rewrite, linear, or forward-chaining rule may have free variables in its
hypotheses, and ACL2 can be directed either to try all bindings
(``:all'') or just the first (``:once'') when relieving that
hypothesis, as a basis for relieving subsequent hypotheses. This directing of
:all or :once is generally provided by specifying either
:match-free :once or :match-free :all in the :rule-classes of the rule. If neither of these is specified, then the most
recent set-match-free-default is used by ACL2 to fill in this missing
:match-free field. See rule-classes. Except: If the last
set-match-free-default specifies nil, then ACL2 reverts to the
behavior it had at start-up, as described in Remarks (2) and (3) below.
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded. It
uses the ACL2-defaults-table, and hence its effect is local to
the book or encapsulate form in which it occurs.
Remarks.
(1) The use of set-match-free-default has no effect on existing rules.
In order to change the behavior of existing rules with respect to
free-variable matching, see add-match-free-override.
(2) If you submit a rewrite, linear, or forward-chaining rule with a free variable in a hypothesis, and no default
setting was previously specified with set-match-free-default or the
default setting is nil, and the rule is not within a book being processed
with include-book, certify-book, or rebuild, then a
warning or error is caused. In order to make this an error instead of a
warning, see set-match-free-error.
(3) If you submit a rewrite, linear, or forward-chaining rule with a free variable in a hypothesis, and no default
setting has been previously specified with set-match-free-default or the
default setting is nil, and no error is caused (see (2) above), then the
default :all is used.
