		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Svex-s4eval

Evaluate an svex in some s4vec environment.

Signature
(svex-s4eval x env) → val
Arguments: x — Expression to evaluate.
Guard (svex-p x).; env — Variable bindings. Must be a fast-alist.
Guard (svex-s4env-p env).
Returns: val — Value of x under this environment.
Type (s4vec-p val).

Like svex-eval but uses s4vec operations instead of 4vec ones.

Theorem: return-type-of-svex-s4eval.val

(defthm return-type-of-svex-s4eval.val
  (b* ((?val (svex-s4eval x env)))
    (s4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-s4eval.vals

(defthm return-type-of-svexlist-s4eval.vals
  (b* ((?vals (svexlist-s4eval x env)))
    (s4veclist-p vals))
  :rule-classes :rewrite)

Function: svex-s4eval-memoize-condition

(defun svex-s4eval-memoize-condition (x env)
  (declare (ignorable x env)
           (xargs :guard
                  (if (svex-p x)
                      (svex-s4env-p env)
                    'nil)))
  (eq (svex-kind x) :call))

Theorem: svex-s4eval-correct

(defthm svex-s4eval-correct
  (b* ((?val (svex-s4eval x env)))
    (equal (s4vec->4vec val)
           (svex-eval x (svex-s4env->svex-env env)))))

Theorem: svexlist-s4eval-correct

(defthm svexlist-s4eval-correct
  (b* ((?vals (svexlist-s4eval x env)))
    (equal (s4veclist->4veclist vals)
           (svexlist-eval x (svex-s4env->svex-env env)))))

Subtopics

Svex-s4xeval: Evaluate an svex using s4vecs in an all-X environment.