Recognizer for svex-reduce-config structures.
(svex-reduce-config-p x) → *
Function:
(defun svex-reduce-config-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'svex-reduce-config-p)) (declare (ignorable acl2::__function__)) (and (std::prod-consp x) (std::prod-consp (std::prod-car x)) (std::prod-consp (std::prod-cdr x)) (b* ((width-extns (std::prod-car (std::prod-car x))) (integerp-extns (std::prod-cdr (std::prod-car x))) (?skip-bitor/and/xor-repeated (std::prod-car (std::prod-cdr x))) (?keep-missing-env-vars (std::prod-cdr (std::prod-cdr x)))) (and (width-of-svex-extn-list-p width-extns) (integerp-of-svex-extn-list-p integerp-extns))))))