A table used to associate function names with macro names
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)
(table macro-aliases-table 'mac 'fn) (defun fn (x) (if (consp x) (mac (cdr x)) x))
Although this is obviously contrived example, this flexibility can be useful to macro writers; see for example the definition of ACL2 system macro defun-inline.
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; see theories.
For example, in order that