		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Binary-op-nonstrictp

Check if a binary operator is non-strict.

Signature
(binary-op-nonstrictp op) → yes/no
Arguments: op — Guard (binary-opp op).
Returns: yes/no — Type (booleanp yes/no).

In Syntheto, some boolean connectives are non-strict, in the sense that one operand can assume the truth or falsehood of the other operand to discharge its type obligations. This is because the value of the result may be determined just by one operand value in some cases. See the static semantics for details.

Definitions and Theorems

Function: binary-op-nonstrictp

(defun binary-op-nonstrictp (op)
  (declare (xargs :guard (binary-opp op)))
  (let ((__function__ 'binary-op-nonstrictp))
    (declare (ignorable __function__))
    (and (member-eq (binary-op-kind op)
                    '(:and :or :implies :implied))
         t)))

Theorem: booleanp-of-binary-op-nonstrictp

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

Theorem: binary-op-nonstrictp-of-binary-op-fix-op

(defthm binary-op-nonstrictp-of-binary-op-fix-op
  (equal (binary-op-nonstrictp (binary-op-fix op))
         (binary-op-nonstrictp op)))

Theorem: binary-op-nonstrictp-binary-op-equiv-congruence-on-op

(defthm binary-op-nonstrictp-binary-op-equiv-congruence-on-op
  (implies (binary-op-equiv op op-equiv)
           (equal (binary-op-nonstrictp op)
                  (binary-op-nonstrictp op-equiv)))
  :rule-classes :congruence)