		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-implementation

Defarbrec-table

Table of defarbrec functions.

For each successful call of defarbrec whose :show-only is not t, this table includes a pair whose key is the name of the generated logic-mode function and whose value contains information about the call (see defarbrec-infop).

This table is used to support the redundancy check in defarbrec-check-redundancy.

Subtopics

Defarbrec-infop: Information about a defarbrec call, recorded as a pair's value in the defarbrec table.
Defarbrec-filter-call: Remove any :print and :show-only options from a call of defarbrec.
*defarbrec-table-name*: Name of the defarbrec table.