ACL2-PC::DIVE

(primitive) move to the indicated subterm
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
(DIVE 1)    -- assign the new current subterm to be the first
               argument of the existing current subterm
(DIVE 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 (dive 1) it is
(+ a b).
If after that, then (dive 2) is invoked, the new current subterm will be
b.
Instead of (dive 1) followed by (dive 2), the same current subterm could be obtained by instead submitting the single instruction (dive 1 2).

General Form:
(dive &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.

Note: Dive is related to the command pp, in that the diving is done according to raw (translated, internal form) syntax. Use the command dv if you want to dive according to the syntax displayed by the command p. Note that (dv n) can be abbreviated by simply n.