		Search-engine friendly clone of the ACL2 documentation.

Operands

Make-operands

Basic constructor macro for operands structures.

Syntax

(make-operands [:op1 <op1>] 
               [:op2 <op2>] 
               [:op3 <op3>] 
               [:op4 <op4>])

This is the usual way to construct operands structures. It simply conses together a structure with the specified fields.

This macro generates a new operands structure from scratch. See also change-operands, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-operands

(defmacro make-operands (&rest args)
  (std::make-aggregate 'operands
                       args
                       '((:op1 quote nil)
                         (:op2 quote nil)
                         (:op3 quote nil)
                         (:op4 quote nil))
                       'make-operands
                       nil))

Function: operands

(defun operands (op1 op2 op3 op4)
  (declare (xargs :guard (and (operand-type-p op1)
                              (operand-type-p op2)
                              (operand-type-p op3)
                              (operand-type-p op4))))
  (declare (xargs :guard t))
  (let ((__function__ 'operands))
    (declare (ignorable __function__))
    (b* ((op1 (mbe :logic (operand-type-fix op1)
                   :exec op1))
         (op2 (mbe :logic (operand-type-fix op2)
                   :exec op2))
         (op3 (mbe :logic (operand-type-fix op3)
                   :exec op3))
         (op4 (mbe :logic (operand-type-fix op4)
                   :exec op4)))
      (std::prod-cons (std::prod-cons op1 op2)
                      (std::prod-cons op3 op4)))))