		Search-engine friendly clone of the ACL2 documentation.

Svex-alist-xeval

Svex-alist-xeval-aux

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

Definitions and Theorems

Function: svex-alist-xeval-aux

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

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

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