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