Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: (add-binop append binary-append)This example associates 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, e.g., (append x y z w) is printed rather than
(binary-append x (binary-append y (binary-append z w))).
The function symbol need not be binary; the name ``add-binop'' is legacy
from when that was the intention. However, the folding of right-associated
arguments suggested above only takes place for binary function symbols.
General Form: (add-binop macro-name function-name)This is a convenient way to add an entry to
macro-aliases-table
and at the same time extend the :binop-table. As suggested by the
example above, right-associated calls of a binary function in this table will
be printed as corresponding calls of macros. Thus in the case of 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, then the effect is
simply to replace f by the corresponding macro symbol.
See macro-aliases-table, see remove-macro-alias, see binop-table, and
see remove-binop.
