File: ACL2-PC_colon__colon_DV.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (62 lines) | stat: -rw-r--r-- 2,029 bytes parent folder | download
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
57
58
59
60
61
62
<html>
<head><title>ACL2-PC_colon__colon_DV.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::DV</h3>(atomic macro)
<code>   </code>move to the indicated subterm
<pre>Major Section:  <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>


<pre>
Examples:
(dv 1)    -- assign the new current subterm to be the first argument
             of the existing current subterm
(dv 1 2)  -- assign the new current subterm to be the result of
             first taking the 1st argument of the existing
             current subterm, and then the 2nd argument of that
</pre>

For example, if the current subterm is

<pre>
(* (+ a b) c),
</pre>

then after <code>(dv 1)</code> it is

<pre>
(+ a b).
</pre>

If after that, then <code>(dv 2)</code> is invoked, the new current subterm
will be

<pre>
b.
</pre>

Instead of <code>(dv 1)</code> followed by <code>(dv 2)</code>, the same current subterm
could be obtained by instead submitting the single instruction
<code>(dv 1 2)</code>.
<p>

<pre>
General Form:
(dv &amp;rest naturals-list)
</pre>

If <code>naturals-list</code> is a non-empty list <code>(n_1 ... n_k)</code> of natural
numbers, let the new current subterm be the result of selecting the
<code>n_1</code>-st argument of the current subterm, and then the <code>n_2</code>-th subterm
of that, ..., finally the <code>n_k</code>-th subterm.<p>

<strong>Note:</strong>  <code>(dv n)</code> may be abbreviated by simply <code>n</code>, so we could have typed
<code>1</code> instead of <code>(dv 1)</code> in the first example above.<p>

<strong>Note:</strong>  See also <code>dive</code>, which is related to the command <code>pp</code>, in that
the diving is done according to raw (translated, internal form)
syntax.  Use the command <code>dv</code> if you want to dive according to the
syntax displayed by the command <code>p</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>