ADD-BINOP

associate a function name with a macro name
Major Section:  SWITCHES-PARAMETERS-AND-MODES-OH-MY

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.