:match-freein 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
:once'') when relieving that hypothesis, as a basis for
relieving subsequent hypotheses. This directing of
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
used by ACL2 to fill in this missing
See rule-classes. Except: If the last
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.
(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
set-match-free-default or the default setting is
and the rule is not within a book being processed with
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
nil, and no error is caused (see (2) above), then the default