ACL2-pc::dv
(atomic macro)
move to the indicated subterm
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
For example, if the current subterm is
(* (+ a b) c),
then after (dv 1) it is
(+ a b).
If after that, then (dv 2) is invoked, the new current subterm will
be
b.
Instead of (dv 1) followed by (dv 2), the same current subterm
could be obtained by instead submitting the single instruction (dv 1
2).
General Form:
(dv &rest naturals-list)
If naturals-list is a non-empty list (n_1 ... n_k) of natural
numbers, let the new current subterm be the result of selecting the
n_1-st argument of the current subterm, and then the n_2-th subterm
of that, ..., finally the n_k-th subterm.
Remark: (dv n) may be abbreviated by simply n, so we could
have typed 1 instead of (dv 1) in the first example above.
Remark: Emacs users who load (into Emacs) the file
emacs-acl2.el (from a suitable directory; see emacs) will have
defined a command, Control-t d, that avoids the need to type dv
commands. After you print the current term using the p or th
command, you may position the cursor on a subterm and type Control-t d.
Emacs will respond by pasting the appropriate dv command immediately
after the interactive proof-builder's prompt. You can then simply type
<RETURN> in order to dive to the desired subterm.
Remark: A similar command is dive, which is related to the
command pp, in that the diving is done according to raw (translated,
internal form) syntax. (See ACL2-pc::dive.) Use the command dv
if you want to dive according to the syntax displayed by the command p.
Thus, the command ``up'' is the inverse of dive, not of dv.
The following example illustrates this point.
ACL2 !>(verify (equal (* a b c) x))
->: p ; print user-level term
(EQUAL (* A B C) X)
->: pp ; print internal-form (translated) term
(EQUAL (BINARY-* A (BINARY-* B C)) X)
->: exit
Exiting....
NIL
ACL2 !>(verify (equal (* a b c) x))
->: p
(EQUAL (* A B C) X)
->: 1 ; same as (dv 1)
->: p ; print user-level term
(* A B C)
->: pp ; print internal-form (translated) term
(BINARY-* A (BINARY-* B C))
->: 3 ; dive to third argument of (* A B C)
->: p
C
->: up ; go up one level in (BINARY-* A (BINARY-* B C))
->: p
(* B C)
->: pp
(BINARY-* B C)
->:
Subtopics
- Dive-into-macros-table
- Right-associated function information for the proof-builder
