		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).

All the binary operators except logical conjunction and disjunction are strict.

Definitions and Theorems

Function: binop-strictp

(defun binop-strictp (op)
  (declare (xargs :guard (binopp op)))
  (let ((__function__ 'binop-strictp))
    (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 :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)