Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: (table macro-aliases-table 'append 'binary-append)This example associates the function symbol
binary-append with the
macro name append. As a result, the name append may be used as a
runic designator (see theories) by the various theory
functions. Thus, for example, it will be legal to write
(in-theory (disable append))as an abbreviation for
(in-theory (disable binary-append))which in turn really abbreviates
(in-theory (set-difference-theories (current-theory :here)
'(binary-append)))
General Form:
(table macro-aliases-table 'macro-name 'function-name)
or very generally
(table macro-aliases-table macro-name-form function-name-form)where
macro-name-form and function-name-form evaluate,
respectively, to a macro name and a function name in the current
ACL2 world. See table for a general discussion of tables and
the table event used to manipulate tables.
The table macro-aliases-table is an alist that associates
macro symbols with function symbols, so that macro names may be used
as runic designators (see theories). For a convenient way to
add entries to this table, see add-macro-alias. To remove
entries from the table with ease, see remove-macro-alias.
This table is used by the theory functions. For example, in order
that (disable append) be interpreted as (disable binary-append),
it is necessary that the example form above has been executed. In
fact, this table does indeed associate many of the macros provided
by the ACL2 system, including append, with function symbols.
Loosely speaking, it only does so when the macro is ``essentially
the same thing as'' a corresponding function; for example,
(append x y) and (binary-append x y) represent the same term,
for any expressions x and y.
