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
|
<html>
<head><title>REMOVE-UNTOUCHABLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>REMOVE-UNTOUCHABLE</h2>remove name or list of names to the list of untouchable symbols
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Examples:
(remove-untouchable my-var nil)
(remove-untouchable set-mem t)
<p>
General Form:
(remove-untouchable name{s} fn-p :doc doc-string)
</pre>
<p>
where <code>name{s}</code> is a non-<code>nil</code> symbol or a non-<code>nil</code> true list of symbols,
<code>fn-p</code> is any value (but generally <code>nil</code> or <code>t</code>), and <code><a href="DOC-STRING.html">doc-string</a></code>
is an optional <a href="DOCUMENTATION.html">documentation</a> string not beginning with
``<code>:doc-section</code> ...''. If <code>name{s}</code> is a symbol it is treated as the
singleton list containing that symbol. The effect of this event is to remove
the given symbols from the list of ``untouchable variables'' in the current
world if <code>fn-p</code> is <code>nil</code>, else to remove the symbols into the list of
``untouchable functions''. This event is redundant if no symbol listed is a
member of the appropriate untouchables list (variables or functions).<p>
Note that <code>remove-untouchable</code> is illegal by default, since it can be used
to provide access to ACL2 internal functions and data structures that are
intentionally made untouchable for the user. If you want to call it, you
must first create an active trust tag; see <a href="DEFTTAG.html">defttag</a>.<p>
Also See <a href="PUSH-UNTOUCHABLE.html">push-untouchable</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>
|
