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
|
<html>
<head><title>DISABLEDP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DISABLEDP</h2>determine whether a given name or rune is disabled
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
Examples:<p>
:disabledp foo ; returns a list of all disabled runes whose base
; symbol is foo (see <a href="RUNE.html">rune</a>)
(disabledp 'foo) ; same as above (i.e., :disabledp foo)
:disabledp (:rewrite bar . 1) ; returns t if the indicated rune is
; disabled, else nil
(disabledp (:rewrite bar . 1)); same as immediately above
</pre>
<p>
Also see <a href="PR.html">pr</a>, which gives much more information about the rules associated
with a given event.<p>
<code>Disabledp</code> takes one argument, an event name (see <a href="EVENTS.html">events</a>) other than
<code>nil</code> or a <a href="RUNE.html">rune</a>. In the former case it returns the list of disabled
runes associated with that name, in the sense that the rune's ``base symbol''
is that name (see <a href="RUNE.html">rune</a>) or, if the event named is a <code><a href="DEFMACRO.html">defmacro</a></code> event,
then the list of disabled runes associated with the function corresponding to
that macro name, if any
(see <a href="MACRO-ALIASES-TABLE.html">macro-aliases-table</a>). In the latter case, where the argument is a
<a href="RUNE.html">rune</a>, <code>disabledp</code> returns <code>t</code> if the rune is disabled, and <code>nil</code>
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>
|
