:match-free in future rules
Major Section: SWITCHES-PARAMETERS-AND-MODES
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.
