		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Svex-alist-eval-for-symbolic

Signature
(svex-alist-eval-for-symbolic x env symbolic-params) → res
Arguments: x — Guard (svex-alist-p x).; env — Guard (svex-env-p env).; symbolic-params — Guard (alistp symbolic-params).
Returns: res — Type (equal res (svex-alist-eval x env)).

Definitions and Theorems

Function: svex-alist-eval-for-symbolic

(defun svex-alist-eval-for-symbolic (x env symbolic-params)
 (declare (xargs :guard (and (svex-alist-p x)
                             (svex-env-p env)
                             (alistp symbolic-params))))
 (let ((__function__ 'svex-alist-eval-for-symbolic))
  (declare (ignorable __function__))
  (mbe
    :logic
    (pairlis$
         (svex-alist-keys x)
         (svexlist-eval-for-symbolic (hons-copy (svex-alist-vals x))
                                     env symbolic-params))
    :exec (svex-alist-eval x env))))

Theorem: return-type-of-svex-alist-eval-for-symbolic

(defthm return-type-of-svex-alist-eval-for-symbolic
  (b* ((res (svex-alist-eval-for-symbolic x env symbolic-params)))
    (equal res (svex-alist-eval x env)))
  :rule-classes :rewrite)