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
46
47
48
49
50
51
52
53
54
55
56
|
<html>
<head><title>TRANS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TRANS</h2>print the macroexpansion of a form
<pre>Major Section: <a href="OTHER.html">OTHER</a>
</pre><p>
<pre>
Examples:
:trans (list a b c)
:trans (caddr x)
:trans (cond (p q) (r))
</pre>
<p>
This function takes one argument, an alleged term, and translates
it, expanding the macros in it completely. Either an error is
caused or the formal meaning of the term is printed. We also print
the ``output signature'' which indicates how many results are returned
and which are single-threaded objects. For example,
a term that returns one ordinary object (e.g., an object other than
<code><a href="STATE.html">STATE</a></code> or a user-defined single-threaded object (see <a href="DEFSTOBJ.html">defstobj</a>))
has the output signature
<pre>
=> *
</pre>
A term that returns the single-threaded object <code>STATE</code> has the
output signature
<pre>
=> STATE
</pre>
and a term that returns four results might have the output signature
<pre>
=> (MV $MEM * * STATE)
</pre>
This signature indicates that the first result is the (user defined)
single-threaded object <code>$MEM</code>, that the next two results are ordinary,
and that the last result is <code>STATE</code>.<p>
See <a href="TRANS_bang_.html">trans!</a> for a corresponding command that does not enforce restrictions of
single-threaded objects.<p>
It is sometimes more convenient to use <code><a href="TRANS1.html">trans1</a></code> which is like trans
but which only does top-level macroexpansion.<p>
For more, see <a href="TERM.html">term</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>
|
