		Search-engine friendly clone of the ACL2 documentation.

Alias-norm.lisp

Assigns-subst-nrev

Signature
(assigns-subst-nrev x aliases svexarr nrev) → nrev
Arguments: x — Guard (assigns-p x).

Definitions and Theorems

Function: assigns-subst-nrev

(defun assigns-subst-nrev (x aliases svexarr nrev)
 (declare (xargs :stobjs (aliases svexarr nrev)))
 (declare (xargs :guard (assigns-p x)))
 (declare
    (xargs :guard (and (svarlist-boundedp (assigns-vars x)
                                          (aliass-length aliases))
                       (svarlist-boundedp (assigns-vars x)
                                          (svexs-length svexarr)))))
 (let ((__function__ 'assigns-subst-nrev))
  (declare (ignorable __function__))
  (b*
   ((x (assigns-fix x))
    ((when (atom x)) (acl2::nrev-fix nrev))
    ((cons lhs (driver rhs)) (car x))
    (lhs (lhs-alias-norm lhs aliases))
    (val (svex-subst-from-svexarr rhs.value svexarr))
    (nrev (acl2::nrev-push (cons lhs (change-driver rhs :value val))
                           nrev)))
   (assigns-subst-nrev (cdr x)
                       aliases svexarr nrev))))