		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-purep

Binop-purep

Signature
(binop-purep binop) → fty::result
Arguments: binop — Guard (binopp binop).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: binop-purep

(defun binop-purep (binop)
  (declare (xargs :guard (binopp binop)))
  (declare (ignorable binop))
  (let ((__function__ 'binop-purep))
    (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
                :asg nil
                :asg-mul nil
                :asg-div nil
                :asg-rem nil
                :asg-add nil
                :asg-sub nil
                :asg-shl nil
                :asg-shr nil
                :asg-and nil
                :asg-xor nil
                :asg-ior nil)))

Theorem: booleanp-of-binop-purep

(defthm booleanp-of-binop-purep
  (b* ((fty::result (binop-purep binop)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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

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

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

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