Return-last-table
Install special raw Lisp behavior
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 use defmacro-last.
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-nil value 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 flet
or macrolet. The 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.