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
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:
the first number in the list given to the interactive proof-builder's
the untranslated term into which we will dive
the translated term into which we will dive
the current ACL2 logical world
The function will normally return a list of positive integers, representing
the (one-based) address for diving into
Referring to the example above,
See table for a general discussion of tables.