		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Pure-binopp

Recognizer pure c$::binops.

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

Definitions and Theorems

Function: pure-binopp

(defun pure-binopp (binop)
 (declare (xargs :guard (binopp binop)))
 (declare (xargs :type-prescription (booleanp (pure-binopp binop))))
 (let ((__function__ 'pure-binopp))
   (declare (ignorable __function__))
   (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)))