# Dive-into-macros-table

Right-associated function information for the proof-builder

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 interactive
proof-builder's DV and numeric diving commands (e.g., 3) in
order to dive properly into subterms. See proof-builder, 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 interactive proof-builder'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 community book books/misc/rtl-untranslate.lisp for the
definition of such a function.

See table for a general discussion of tables.

### Subtopics

- Remove-dive-into-macro
- Removes association of proof-builder diving function with macro name
- Add-dive-into-macro
- Associate proof-builder diving function with macro name