Major Section: SWITCHES-PARAMETERS-AND-MODES
Please first see return-last for relevant background.
This table is for advanced users only, and requires an active trust
tag (see defttag). We recommend that you do not modify this table directly,
but instead use the macro
defmacro-last. Here we augment that discussion
with some highly technical observations that can probably be ignored if you
This table has a
:guard requiring that each key be a symbol defined
in raw Lisp, generally as a macro, and requiring that each non-
be associated either with a symbol that names a macro defined in ACL2, or
else with a list of one element containing such a symbol. The table can only
be modified when there is an active trust tag; see defttag. If a key is
associated with the value
nil, then that key is treated as though it were
not in the table.
Note that keys of this table are not eligible to be bound by
current value of this table may be obtained by evaluating the form
(table-alist 'return-last-table (w state)). The built-in constant
*initial-return-last-table* holds the initial value of this table.