## DIVE-INTO-MACROS-TABLE

right-associated function information for the proof-checker
Major Section: SWITCHES-PARAMETERS-AND-MODES

Examples:
ACL2 !>(dive-into-macros-table (w state))
((CAT . EXPAND-ADDRESS-CAT)
(LXOR . EXPAND-ADDRESS-LXOR)

This table associates macro names with functions used by the
proof-checker's `DV`

and numeric diving commands (e.g., `3`

) in
order to dive properly into subterms. See proof-checker, in particular the
documentation for `DV`

.
This table can be extended easily. See add-dive-into-macro and also
see remove-dive-into-macro.

The symbol associated with a macro should be a function symbol taking four
arguments, in this order:

`car-addr`

; the first number in the list given to the proof-checker's
`DV`

command
`raw-term`

; the untranslated term into which we will dive
`term`

; the translated term into which we will dive
`wrld`

; the current ACL2 logical world

The function will normally return a list of positive integers, representing
the (one-based) address for diving into `term`

that corresponds to the
single-address dive into `raw-term`

by `car-address`

. However, it can
return `(cons str alist)`

, where `str`

is a string suitable for `fmt`

and `args`

is the corresponding alist for `fmt`

.
Referring to the example above, `expand-address-cat`

would be such a
function, which will be called on `raw-term`

values that are calls of
`cat`

. See the distributed book `books/misc/rtl-untranslate.lisp`

for
the definition of such a function.

See table for a general discussion of tables.