		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-eval

4v-sexpr-eval-list-list

Definitions and Theorems

Function: 4v-sexpr-eval-list-list1

(defun 4v-sexpr-eval-list-list1 (x env)
       "Assumes ENV is fast"
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (cons (4v-sexpr-eval-list (car x) env)
                 (4v-sexpr-eval-list-list1 (cdr x)
                                           env))))

Function: 4v-sexpr-eval-list-list

(defun
 4v-sexpr-eval-list-list (x env)
 "Makes ENV fast if necessary"
 (declare (xargs :guard t))
 (mbe :logic (if (atom x)
                 nil
                 (cons (4v-sexpr-eval-list (car x) env)
                       (4v-sexpr-eval-list-list (cdr x) env)))
      :exec (with-fast-alist env (4v-sexpr-eval-list-list1 x env))))

Theorem: 4v-sexpr-eval-list-list1-removal

(defthm 4v-sexpr-eval-list-list1-removal
        (equal (4v-sexpr-eval-list-list1 x env)
               (4v-sexpr-eval-list-list x env)))