1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
<html>
<head><title>SET-MATCH-FREE-DEFAULT.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-MATCH-FREE-DEFAULT</h2>provide default for <code>:match-free</code> in future rules
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
General Forms:
(set-match-free-default :once)
(set-match-free-default :all)
(set-match-free-default nil)
</pre>
<p>
As described elsewhere (see <a href="FREE-VARIABLES.html">free-variables</a>), a <a href="REWRITE.html">rewrite</a>, <a href="LINEAR.html">linear</a>, or
<a href="FORWARD-CHAINING.html">forward-chaining</a> rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (``<code>:all</code>'') or just the
first (``<code>:once</code>'') when relieving that hypothesis, as a basis for
relieving subsequent hypotheses. This direction of <code>:all</code> or <code>:once</code> is
generally provided by specifying either <code>:match-free :once</code> or
<code>:match-free :all</code> in the <code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code> of the rule. If neither
of these is specified, then the most recent <code>set-match-free-default</code> is
used by ACL2 to fill in this missing <code>:match-free</code> field.
See <a href="RULE-CLASSES.html">rule-classes</a>. Except: If the last <code>set-match-free-default</code> specifies
<code>nil</code>, then ACL2 reverts to the behavior it had at start-up, as described
in Remarks (2) and (3) below.<p>
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical <a href="WORLD.html">world</a> and is so
recorded. It uses the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>, and hence its effect is
<code><a href="LOCAL.html">local</a></code> to the book or <code><a href="ENCAPSULATE.html">encapsulate</a></code> form in which it occurs.
<p>
Remarks.<p>
(1) The use of <code>set-match-free-default</code> has no effect on existing rules. In
order to change the behavior of existing rules with respect to free-variable
matching, see <a href="ADD-MATCH-FREE-OVERRIDE.html">add-match-free-override</a>.<p>
(2) If you submit a <a href="REWRITE.html">rewrite</a>, <a href="LINEAR.html">linear</a>, or <a href="FORWARD-CHAINING.html">forward-chaining</a> rule
with a free variable in a hypothesis, and no default setting was previously
specified with <code>set-match-free-default</code> or the default setting is <code>nil</code>,
and the rule is not within a book being processed with <code><a href="INCLUDE-BOOK.html">include-book</a></code>,
<code><a href="CERTIFY-BOOK.html">certify-book</a></code>, or <code><a href="REBUILD.html">rebuild</a></code>, then a warning or error is caused. In
order to make this an error instead of a warning, see <a href="SET-MATCH-FREE-ERROR.html">set-match-free-error</a>.<p>
(3) If you submit a <a href="REWRITE.html">rewrite</a>, <a href="LINEAR.html">linear</a>, or <a href="FORWARD-CHAINING.html">forward-chaining</a> rule
with a free variable in a hypothesis, and no default setting has been
previously specified with <code>set-match-free-default</code> or the default setting
is <code>nil</code>, and no error is caused (see (2) above), then the default <code>:all</code>
is used.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
