		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-partial-eval-list

(aig-partial-eval-list x env) partially evaluates a list of AIGs.

Signature
(aig-partial-eval-list x env) → aig-list
Arguments: x — List of AIGs.; env — Fast alist binding variables to Booleans, as in aig-partial-eval.

Definitions and Theorems

Function: aig-partial-eval-list

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