Basic constructor macro for op/en-p structures.
(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.
This is an ordinary
Macro:
(defmacro make-op/en-p (&rest args) (std::make-aggregate 'op/en-p args '((:src1) (:src2) (:src3) (:src4)) 'make-op/en-p nil))
Function:
(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)))))