		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Binop-purep

Check if a binary operator is pure.

Signature
(binop-purep op) → yes/no
Arguments: op — Guard (binopp op).
Returns: yes/no — Type (booleanp yes/no).

All the binary operators except (simple and compound) assignments are pure.

Definitions and Theorems

Function: binop-purep

(defun binop-purep (op)
  (declare (xargs :guard (binopp op)))
  (let ((__function__ 'binop-purep))
    (declare (ignorable __function__))
    (and (member-eq (binop-kind op)
                    (list :mul :div
                          :rem :add
                          :sub :shl
                          :shr :lt
                          :gt :le
                          :ge :eq
                          :ne :bitand
                          :bitxor :bitior
                          :logand :logor))
         t)))

Theorem: booleanp-of-binop-purep

(defthm booleanp-of-binop-purep
  (b* ((yes/no (binop-purep op)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: binop-purep-of-binop-fix-op

(defthm binop-purep-of-binop-fix-op
  (equal (binop-purep (binop-fix op))
         (binop-purep op)))

Theorem: binop-purep-binop-equiv-congruence-on-op

(defthm binop-purep-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (binop-purep op)
                  (binop-purep op-equiv)))
  :rule-classes :congruence)