associate a binary function name with a macro name
Major Section:  EVENTS

(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))).

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. See macro-aliases-table, see remove-macro-alias, see binop-table, and see remove-binop.