		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-alist-compose-nrev

Signature
(svex-alist-compose-nrev x a nrev) → nrev
Arguments: x — Guard (svex-alist-p x).; a — Guard (svex-alist-p a).

Definitions and Theorems

Function: svex-alist-compose-nrev

(defun svex-alist-compose-nrev (x a nrev)
 (declare (xargs :stobjs (nrev)))
 (declare (xargs :guard (and (svex-alist-p x)
                             (svex-alist-p a))))
 (let ((__function__ 'svex-alist-compose-nrev))
  (declare (ignorable __function__))
  (if (atom x)
      (acl2::nrev-fix nrev)
    (if (mbt (and (consp (car x)) (svar-p (caar x))))
        (b* ((nrev (acl2::nrev-push (cons (caar x)
                                          (svex-compose (cdar x) a))
                                    nrev)))
          (svex-alist-compose-nrev (cdr x)
                                   a nrev))
      (svex-alist-compose-nrev (cdr x)
                               a nrev)))))