		Search-engine friendly clone of the ACL2 documentation.

Svex-alist-eval

Svex-alist-eval-aux

Signature
(svex-alist-eval-aux x env) → xx
Arguments: x — Guard (svex-alist-p x).; env — Guard (svex-env-p env).
Returns: xx — Type (svex-env-p xx).

Definitions and Theorems

Function: svex-alist-eval-aux

(defun svex-alist-eval-aux (x env)
  (declare (xargs :guard (and (svex-alist-p x)
                              (svex-env-p env))))
  (let ((__function__ 'svex-alist-eval-aux))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbt (and (consp (car x)) (svar-p (caar x))))
          (cons (cons (caar x) (svex-eval (cdar x) env))
                (svex-alist-eval-aux (cdr x) env))
        (svex-alist-eval-aux (cdr x) env)))))

Theorem: svex-env-p-of-svex-alist-eval-aux

(defthm svex-env-p-of-svex-alist-eval-aux
  (b* ((xx (svex-alist-eval-aux x env)))
    (svex-env-p xx))
  :rule-classes :rewrite)