Major Section: SWITCHES-PARAMETERS-AND-MODES
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 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.
