associate a function name with a macro name

(add-macro-fn append binary-append)
(add-macro-fn append binary-append t)
These examples each associate the function symbol binary-append with the macro name append. As a result, theory functions will understand that append refers to binary-append -- see add-macro-alias -- and moreover, proof output will be printed using append rather than binary-append. In the first case, (append x (append y z)) is printed rather than (append x y z). In the second case, right-associated arguments are printed flat: (append x y z). Such right-association is considered only for binary function symbols; otherwise the optional third argument is ignored.

General Forms:
(add-macro-fn macro-name function-name)
(add-macro-fn macro-name function-name nil) ; same as abov
(add-macro-fn macro-name function-name t)

This is a convenient way to add an entry to macro-aliases-table and at the same time extend the untrans-table. As suggested by the example above, calls of a function in this table will be printed as corresponding calls of macros, with right-associated arguments printed flat in the case of a binary function symbol if the optional third argument is t. In that case, for a binary function symbol fn associated with macro name mac, then a call (fn arg1 (fn arg2 (... (fn argk arg)))) will be displayed to the user as though the ``term'' were (mac arg1 arg2 ... argk arg). For a call (f a1 ... ak) of a function symbol that is not binary, or the optional argument is not supplied as t, then the effect is simply to replace f by the corresponding macro symbol. See add-macro-alias, which is invoked on the first two arguments. Also see remove-macro-alias, see untrans-table, and see remove-macro-fn.