		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-compose-list

(aig-compose-list x sigma) composes into a list of AIGs.

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

Definitions and Theorems

Function: aig-compose-list

(defun aig-compose-list (x sigma)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-compose-list))
            (declare (ignorable __function__))
            (if (atom x)
                nil
                (cons (aig-compose (car x) sigma)
                      (aig-compose-list (cdr x) sigma)))))