SET-MATCH-FREE-DEFAULT

Major Section:  EVENTS

General Forms:
(set-match-free-default :once)
(set-match-free-default :all)
(set-match-free-default nil)

As described elsewhere (see free-variables), a rewrite or linear 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 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. 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 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 or linear 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 or certify-book, then an error or warning is caused. In order to make this a warning instead of an error, see set-match-free-error.

(3) If you submit a rewrite or linear 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.