		Search-engine friendly clone of the ACL2 documentation.

Operands

Operands-p

Recognizer for operands structures.

Signature
(operands-p x) → *

Definitions and Theorems

Function: operands-p

(defun operands-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'operands-p))
    (declare (ignorable __function__))
    (and (std::prod-consp x)
         (std::prod-consp (std::prod-car x))
         (std::prod-consp (std::prod-cdr x))
         (b* ((op1 (std::prod-car (std::prod-car x)))
              (op2 (std::prod-cdr (std::prod-car x)))
              (op3 (std::prod-car (std::prod-cdr x)))
              (op4 (std::prod-cdr (std::prod-cdr x))))
           (and (operand-type-p op1)
                (operand-type-p op2)
                (operand-type-p op3)
                (operand-type-p op4))))))