		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)))