		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-restrict-list

(aig-restrict-list x sigma) substitutes into a list of AIGs.

Signature
(aig-restrict-list x sigma) → aig-list
Arguments: x — List of AIGs.; sigma — Fast alist binding variables to replacement AIGs, as in aig-restrict.

Definitions and Theorems

Function: aig-restrict-list

(defun
     aig-restrict-list (x sigma)
     (declare (xargs :guard t))
     (let ((__function__ 'aig-restrict-list))
          (declare (ignorable __function__))
          (mbe :logic (if (atom x)
                          nil
                          (cons (aig-restrict (car x) sigma)
                                (aig-restrict-list (cdr x) sigma)))
               :exec (aig-restrict-list-acc x sigma nil))))