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
|
<html>
<head><title>ACL2-PC_colon__colon_EXPAND.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::EXPAND</h3>(primitive)
<code> </code>expand the current function call without simplification
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
expand -- expand and do not simplify.
</pre>
For example, if the current subterm is <code>(append a b)</code>, then after
<code>(expand t)</code> the current subterm will be the term:
<pre>
(if (true-listp x)
(if x
(cons (car x) (append (cdr x) y))
y)
(apply 'binary-append (list x y)))
</pre>
regardless of the top-level hypotheses and the governors.
<p>
<pre>
General Form:
(expand &optional do-not-expand-lambda-flg)
</pre>
Expand the function call at the current subterm, and do not
simplify. The options have the following meanings:
<pre>
do-not-expand-lambda-flg: default is nil; otherwise, the result
should be a lambda expression<p>
</pre>
See also <code>x</code>, which allows simplification.
<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>
|
