		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Binop-strictp

Check if a binary operator is strict.

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

These are all the binary operators except logical conjunction and disjunction.

Definitions and Theorems

Function: binop-strictp

(defun binop-strictp (op)
  (declare (xargs :guard (binopp op)))
  (and (member-eq (binop-kind op)
                  (list :mul
                        :div :rem
                        :add :sub
                        :shl :shr
                        :lt :gt
                        :le :ge
                        :eq :ne
                        :bitand :bitxor
                        :bitior :asg
                        :asg-mul :asg-div
                        :asg-rem :asg-add
                        :asg-sub :asg-shl
                        :asg-shr :asg-and
                        :asg-xor :asg-ior))
       t))

Theorem: booleanp-of-binop-strictp

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

Theorem: binop-strictp-of-binop-fix-op

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

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

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