		Search-engine friendly clone of the ACL2 documentation.

Macros

Add-macro-alias

Associate a function name with a macro name

Example:
(add-macro-alias 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. See add-macro-fn and add-binop for extensions of this utility that also affect printing.

General Form:
(add-macro-alias macro-name sym)

where macro-name is a macro name and sym is a symbol. If sym is a function symbol, then this event establishes macro-name as a macro-alias for sym by associating macro-name with sym in the table, macro-aliases-table; see macro-aliases-table for detailed discussion. In particular, that discussion explains the use of macro-aliases to allow a macro name as the second argument of add-macro-alias, as in the example below.

(defun fn (x) x)
(defmacro mac1 (x) (fn x))
(defmacro mac2 (x) (list 'mac1 x))
(add-macro-alias mac1 fn); or (table macro-aliases-table 'mac1 'fn)

; The following is equivalent to (add-macro-alias mac2 fn), since
; mac1 is a macro-alias for fn by virtue of the preceding event.
; Note that the form (table macro-aliases-table 'mac2 'mac1)
; would not suffice here; that is, the in-theory event below would cause an
; error, because mac1 is not a function symbol.
(add-macro-alias mac2 mac1)

; Success:
(in-theory (disable mac2))

Also see macro-aliases-table and also see remove-macro-alias.