Basic constructor macro for svex-reduce-config structures.
(make-svex-reduce-config [:width-extns <width-extns>] [:integerp-extns <integerp-extns>] [:skip-bitor/and/xor-repeated <skip-bitor/and/xor-repeated>] [:keep-missing-env-vars <keep-missing-env-vars>])
This is the usual way to construct svex-reduce-config structures. It simply conses together a structure with the specified fields.
This macro generates a new svex-reduce-config structure from scratch. See also change-svex-reduce-config, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-svex-reduce-config (&rest args) (std::make-aggregate 'svex-reduce-config args '((:width-extns) (:integerp-extns) (:skip-bitor/and/xor-repeated) (:keep-missing-env-vars)) 'make-svex-reduce-config nil))
Function:
(defun svex-reduce-config (width-extns integerp-extns skip-bitor/and/xor-repeated keep-missing-env-vars) (declare (xargs :guard (and (width-of-svex-extn-list-p width-extns) (integerp-of-svex-extn-list-p integerp-extns)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'svex-reduce-config)) (declare (ignorable acl2::__function__)) (b* ((width-extns (mbe :logic (width-of-svex-extn-list-fix width-extns) :exec width-extns)) (integerp-extns (mbe :logic (integerp-of-svex-extn-list-fix integerp-extns) :exec integerp-extns))) (std::prod-cons (std::prod-cons width-extns integerp-extns) (std::prod-cons skip-bitor/and/xor-repeated keep-missing-env-vars)))))