Add-macro-fn
Associate a function name with a macro name
Examples:
(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 above
(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.
