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