Recognizer for svex-scc-consts structures.
(svex-scc-consts-p x) → *
Function:
(defun svex-scc-consts-p (x) (declare (xargs :guard t)) (let ((__function__ 'svex-scc-consts-p)) (declare (ignorable __function__)) (and (std::prod-consp x) (std::prod-consp (std::prod-car x)) (std::prod-consp (std::prod-cdr x)) (b* ((final-masks (std::prod-car (std::prod-car x))) (loop-vars (std::prod-cdr (std::prod-car x))) (compose-iter-limit (std::prod-car (std::prod-cdr x))) (updates (std::prod-cdr (std::prod-cdr x)))) (and (svex-mask-alist-p final-masks) (svar-key-alist-p loop-vars) (maybe-natp compose-iter-limit) (svex-alist-p updates))))))