		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-restrict-alists

(aig-restrict-alists x sigma) substitutes into a list of AIG Alists.

Signature
(aig-restrict-alists x sigma) → aig-alists
Arguments: x — List of AIG alists, which need not be fast.; sigma — Fast alist binding variables to replacement AIGs, as in aig-restrict.
Returns: aig-alists — List of ordinary (slow) alists, derived from x via aig-restrict-alist.

Definitions and Theorems

Function: aig-restrict-alists

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