		Search-engine friendly clone of the ACL2 documentation.

Faig-eval

Faig-eval-alist

(faig-eval-list x env) evaluates an FAIG alist (an alist binding keys to FAIGs).

Signature
(faig-eval-alist x env) → *

The alist x does not need to be fast, and we produce an ordinary (slow) alist as a result.

Definitions and Theorems

Function: faig-eval-alist

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

Subtopics

Faig-eval-alist-thms: Basic theorems about faig-eval-alist.