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