		Search-engine friendly clone of the ACL2 documentation.

Aig-semantics

Aig-eval-alists

Evaluate a list of AIG Alists.

Signature
(aig-eval-alists x env) → vals-alists
Arguments: x — List of AIG Alists to evaluate.; env — The environment to use; see aig-eval.
Returns: vals-alists — A copy of x, except that each AIG has been replaced with its value.

Definitions and Theorems

Function: aig-eval-alists

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