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-IGNORE-OK.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SET-IGNORE-OK</h2>allow unused formals and locals without an <code>ignore</code> or <code>ignorable</code> declaration
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Examples:
(set-ignore-ok t)
(set-ignore-ok nil)
(set-ignore-ok :warn)
</pre>
The first example above allows unused formals and locals, i.e., variables
that would normally have to be <a href="DECLARE.html">declare</a>d <code>ignore</code>d or <code>ignorable</code>.
The second example disallows unused formals and locals; this is the default.
The third example allows them, but prints an appropriate warning.<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. Moreover, its effect is to set 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
containing it; see <a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a>.
<p>
<pre>
General Form:
(set-ignore-ok flg)
</pre>
where <code>flg</code> is either <code>t</code>, <code>nil</code>, or <code>:warn</code>.<p>
One might find this event useful when one is generating function
definitions by an automated procedure, when that procedure does not
take care to make sure that all formals are actually used in the
definitions that it generates.<p>
Note: Defun will continue to report irrelevant formals even if
<code>:set-ignore-ok</code> has been set to <code>t</code>, unless you also use
<code><a href="SET-IRRELEVANT-FORMALS-OK.html">set-irrelevant-formals-ok</a></code> to instruct it otherwise.
<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>
|
