		Search-engine friendly clone of the ACL2 documentation.

Op/en-p

Make-op/en-p

Basic constructor macro for op/en-p structures.

Syntax

(make-op/en-p [:src1 <src1>] 
              [:src2 <src2>] 
              [:src3 <src3>] 
              [:src4 <src4>])

This is the usual way to construct op/en-p structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-op/en-p

(defmacro make-op/en-p (&rest args)
  (std::make-aggregate 'op/en-p
                       args '((:src1) (:src2) (:src3) (:src4))
                       'make-op/en-p
                       nil))

Function: op/en-p

(defun op/en-p (src1 src2 src3 src4)
  (declare (xargs :guard (and (acl2::keyword-listp src1)
                              (acl2::keyword-listp src2)
                              (acl2::keyword-listp src3)
                              (acl2::keyword-listp src4))))
  (declare (xargs :guard t))
  (let ((__function__ 'op/en-p))
    (declare (ignorable __function__))
    (b* ((src1 (mbe :logic (keyword-list-fix src1)
                    :exec src1))
         (src2 (mbe :logic (keyword-list-fix src2)
                    :exec src2))
         (src3 (mbe :logic (keyword-list-fix src3)
                    :exec src3))
         (src4 (mbe :logic (keyword-list-fix src4)
                    :exec src4)))
      (list (cons 'src1 src1)
            (cons 'src2 src2)
            (cons 'src3 src3)
            (cons 'src4 src4)))))