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