(constraintlist-subst-from-svexarr-nrev x aliases svexarr nrev) → nrev
Function:
(defun constraintlist-subst-from-svexarr-nrev (x aliases svexarr nrev) (declare (xargs :stobjs (aliases svexarr nrev))) (declare (xargs :guard (constraintlist-p x))) (declare (xargs :guard (and (svarlist-boundedp (constraintlist-vars x) (aliass-length aliases)) (svarlist-boundedp (constraintlist-vars x) (svexs-length svexarr))))) (let ((__function__ 'constraintlist-subst-from-svexarr-nrev)) (declare (ignorable __function__)) (b* (((when (atom x)) (acl2::nrev-fix nrev)) ((constraint x1) (car x)) (cond (svex-subst-from-svexarr x1.cond svexarr)) (nrev (acl2::nrev-push (change-constraint x1 :cond cond) nrev))) (constraintlist-subst-from-svexarr-nrev (cdr x) aliases svexarr nrev))))