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
|
<html>
<head><title>SET-MATCH-FREE-ERROR.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-MATCH-FREE-ERROR</h2>control error vs. warning when <code>:match-free</code> is missing
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Legal Forms:
(set-match-free-error nil)
:set-match-free-error nil
(set-match-free-error t)
:set-match-free-error t
</pre>
<p>
As described elsewhere (see <a href="FREE-VARIABLES.html">free-variables</a>), when a <a href="REWRITE.html">rewrite</a>,
<a href="LINEAR.html">linear</a>, or <a href="FORWARD-CHAINING.html">forward-chaining</a> rule has free variables in its
hypotheses, the user can specify whether to try all bindings
(``<code>:all</code>'') or just the first (``<code>:once</code>'') when relieving its
hypotheses, as a basis for relieving subsequent hypotheses. This direction
of <code>:all</code> or <code>:once</code> is generally provided by specifying either
<i>:match-free :once</i> or <i>:match-free :all</i> in the <code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code>
of the rule.<p>
But suppose that neither of these is specified, and that
<code>set-match-free-default</code> has not specified a default of <code>:once</code> or
<code>:all</code> (see <a href="SET-MATCH-FREE-DEFAULT.html">set-match-free-default</a>). In this case a warning will occur
except when in the context of <code><a href="INCLUDE-BOOK.html">include-book</a></code>. If you prefer to see an
error in such cases, except in the context of <code><a href="CERTIFY-BOOK.html">certify-book</a></code>, execute
<code>(set-match-free-error t)</code>. If there is no error, then a default of
<code>:all</code> is used.
<p>
Note: This is NOT an event! Instead, <code>set-match-free-error</code> sets the
state global <code>'match-free-error</code> (see <a href="STATE.html">state</a> and see <a href="ASSIGN.html">assign</a>). Thus, this
form cannot be put into a book. If you are tempted to put it into a book,
consider the fact that it really isn't needed there, since the absence of
<code>:match-free</code> does not cause an error in the context of <code><a href="CERTIFY-BOOK.html">certify-book</a></code>
or <code><a href="INCLUDE-BOOK.html">include-book</a></code>. If you still feel the need for such a form, consider
using <code>set-match-free-default</code> to provide a default, at least within the
scope of the current book (if any); see <a href="SET-MATCH-FREE-DEFAULT.html">set-match-free-default</a>.
<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>
|
