		Search-engine friendly clone of the ACL2 documentation.

Defmapping-implementation

Defmapping-table

Table of recorded defmapping information.

For each successful call of defmapping whose :show-only input is not t, this table includes a pair whose key is the name supplied as first input to defmapping and whose value includes the information about the domains, conversions, and theorems (see defmapping-infop).

This table is used not only to record the defmapping information, but also to support the redundancy check in defmapping-check-redundancy.

Subtopics

Defmapping-infop: Information about a defmapping call, recorded as a pair's value in the defmapping table.
Defmapping-lookup: Return the information for the defmapping specified by name, or nil if there is no defmapping with that name.
Defmapping-filter-call: Remove any :print and :show-only inputs from a call of defmapping or its wrappers.
Maybe-defmapping-infop: Recognize information about a defmapping call, and nil.
*defmapping-table-name*: Name of the defmapping table.