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