|
|
|---|
|
|
|
|---|
Basic constructor macro for header-name-quotes structures.
(make-header-name-quotes [:chars <chars>])
This is the usual way to construct header-name-quotes structures. It simply conses together a structure with the specified fields.
This macro generates a new header-name-quotes structure from scratch. See also change-header-name-quotes, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-header-name-quotes (&rest args) (std::make-aggregate 'header-name-quotes args '((:chars)) 'make-header-name-quotes nil))
Function:
(defun header-name-quotes (chars) (declare (xargs :guard (q-char-listp chars))) (declare (xargs :guard t)) (b* ((chars (mbe :logic (q-char-list-fix chars) :exec chars))) (cons :quotes chars)))