ADD-BINOP
associate a binary function name with a macro name
Major Section: EVENTS
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))).
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.
