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