Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: (add-binop append binary-append)This example associates the function symbol
binary-appendwith the macro name
append. As a result, theory functions will understand that
binary-append-- see add-macro-alias -- and moreover, proof output will be printed using
(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-tableand 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
fnassociated 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
fby the corresponding macro symbol. See macro-aliases-table, see remove-macro-alias, see binop-table, and see remove-binop.