		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-partial-eval-alist

(aig-partial-eval-alist x env) partially evaluates an AIG Alist (an alist binding keys to AIGs).

Signature
(aig-partial-eval-alist x env) → aig-alist
Arguments: x — Alist binding names to AIGs. This doesn't need to be a fast alist.; env — Fast alist binding variables to Booleans, as in aig-partial-eval.
Returns: aig-alist — Ordinary (slow) alist with the same keys as x, and values formed by restricting each aig with aig-partial-eval.

Definitions and Theorems

Function: aig-partial-eval-alist

(defun aig-partial-eval-alist (x env)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-partial-eval-alist))
            (declare (ignorable __function__))
            (cond ((atom x) nil)
                  ((atom (car x))
                   (aig-partial-eval-alist (cdr x) env))
                  (t (cons (cons (caar x)
                                 (aig-partial-eval (cdar x) env))
                           (aig-partial-eval-alist (cdr x)
                                                   env))))))

Theorem: alistp-of-aig-partial-eval-alist

(defthm alistp-of-aig-partial-eval-alist
        (alistp (aig-partial-eval-alist x env)))

Subtopics

Aig-partial-eval-alist-thms: Basic theorems about aig-partial-eval-alist.