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
|
<html>
<head><title>ACL2-PC_colon__colon_UP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::UP</h3>(primitive)
<code> </code>move to the parent (or some ancestor) of the current subterm
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples: if the conclusion is (= x (* (- y) z)) and the
current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2) -- the current subterm becomes (* (- y) z)
(up 3) -- the current subterm becomes the entire conclusion
(up 4) -- no change; can't go up that many levels
<p>
General Form:
(up &optional n)
</pre>
Move up <code>n</code> levels in the conclusion from the current subterm, where <code>n</code>
is a positive integer. If <code>n</code> is not supplied or is <code>nil</code>, then move up
1 level, i.e., treat the instruction as <code>(up 1)</code>.<p>
See also <code>dive</code>, <code>top</code>, <code>nx</code>, and <code>bk</code>.
<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>
|
