		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-eval

4v-sexpr-eval-alists

Definitions and Theorems

Function: 4v-sexpr-eval-alists1

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

Function: 4v-sexpr-eval-alists

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

Theorem: 4v-sexpr-eval-alists1-removal

(defthm 4v-sexpr-eval-alists1-removal
  (equal (4v-sexpr-eval-alists1 x env)
         (4v-sexpr-eval-alists x env)))