Basic constructor macro for structdecl-member structures.
(make-structdecl-member [:extension <extension>] [:specqual <specqual>] [:declor <declor>])
This is the usual way to construct structdecl-member structures. It simply conses together a structure with the specified fields.
This macro generates a new structdecl-member structure from scratch. See also change-structdecl-member, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-structdecl-member (&rest args) (std::make-aggregate 'structdecl-member args '((:extension) (:specqual) (:declor)) 'make-structdecl-member nil))
Function:
(defun structdecl-member (extension specqual declor) (declare (xargs :guard (and (booleanp extension) (specqual-listp specqual) (structdeclor-listp declor)))) (declare (xargs :guard t)) (let ((__function__ 'structdecl-member)) (declare (ignorable __function__)) (b* ((extension (mbe :logic (acl2::bool-fix extension) :exec extension)) (specqual (mbe :logic (specqual-list-fix specqual) :exec specqual)) (declor (mbe :logic (structdeclor-list-fix declor) :exec declor))) (cons :member (list extension specqual declor)))))