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