		Search-engine friendly clone of the ACL2 documentation.

Faig-eval

Faig-eval-list

(faig-eval-list x env) evaluates a list of FAIGs.

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

Definitions and Theorems

Function: faig-eval-list

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

Theorem: nth-of-faig-eval-list

(defthm nth-of-faig-eval-list
  (faig-const-equiv (nth n (faig-eval-list x env))
                    (faig-eval (nth n x) env)))