		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Pure-binopp

Recognizer pure c$::binops.

Signature
(pure-binopp binop) → *
Arguments: binop — Guard (c$::binopp binop).

Definitions and Theorems

Function: pure-binopp

(defun pure-binopp (binop)
 (declare (xargs :guard (c$::binopp binop)))
 (declare (xargs :type-prescription (booleanp (pure-binopp binop))))
 (let ((__function__ 'pure-binopp))
   (declare (ignorable __function__))
   (c$::binop-case binop
                   :mul t
                   :div t
                   :rem t
                   :add t
                   :sub t
                   :shl t
                   :shr t
                   :lt t
                   :gt t
                   :le t
                   :ge t
                   :eq t
                   :ne t
                   :bitand t
                   :bitxor t
                   :bitior t
                   :logand t
                   :logor t
                   :otherwise nil)))