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>SHOW-BODIES.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SHOW-BODIES</h2>show the potential definition bodies
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
Examples:
(show-bodies foo)
:show-bodies foo
</pre>
A definition made using <code><a href="DEFUN.html">defun</a></code> installs a so-called ``body'' of a
function symbol, as do certain <code>:</code><code><a href="DEFINITION.html">definition</a></code> rules. Such bodies are
used in a number of ways, including the application of <code>:expand</code>
<a href="HINTS.html">hints</a>; see <a href="DEFINITION.html">definition</a>, in particular the discussion of ``body'' there,
and see <a href="HINTS.html">hints</a> for a discussion of the <code>:expand</code> hint. Also see <a href="SET-BODY.html">set-body</a>
for how to change which of the available definitions (among the original
definition and appropriate <code>:</code><code><a href="DEFINITION.html">definition</a></code> rules) is the one that
provides the body. The <code>show-bodies</code> command displays the available such
bodies in an appropriate format, starting with the one that is currently used
as the body.<p>
<pre>
General Forms:
(show-bodies function-symbol)
:show-bodies function-symbol
</pre>
<p>
<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>
|
