|
|
|---|
|
|
|
|---|
List of (the names of) the ACL2 functions that model Java primitive binary operations.
These are all the binary boolean, integer, and floating-point operations.
Definition:
(defconst *atj-jprim-binop-fns* '(boolean-and boolean-xor boolean-ior boolean-eq boolean-neq int-add long-add int-sub long-sub int-mul long-mul int-div long-div int-rem long-rem int-and long-and int-xor long-xor int-ior long-ior int-eq long-eq int-neq long-neq int-less long-less int-lesseq long-lesseq int-great long-great int-greateq long-greateq int-int-shiftl long-long-shiftl long-int-shiftl int-long-shiftl int-int-shiftr long-long-shiftr long-int-shiftr int-long-shiftr int-int-ushiftr long-long-ushiftr long-int-ushiftr int-long-ushiftr float-add double-add float-sub double-sub float-mul double-mul float-div double-div float-rem double-rem float-eq double-eq float-neq double-neq float-less double-less float-lesseq double-lesseq float-great double-great float-greateq double-greateq))