BINOP-TABLE

associates binary function with the corresponding macro 
Major Section:  MISCELLANEOUS


Examples:
ACL2 !>(binop-table (w state))
'((binary-+ . +)
  (binary-* . *)
  (binary-append . append)
  (binary-logand . logand)
  (binary-logior . logior)
  (binary-logxor . logxor)
  (binary-logeqv . logeqv))

See add-binop for a more general discussion.