		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Svexlist-evals-equal

Signature
(svexlist-evals-equal x env1 env2) → *
Arguments: x — Guard (svexlist-p x).; env1 — Guard (svex-env-p env1).; env2 — Guard (svex-env-p env2).

Definitions and Theorems

Function: svexlist-evals-equal

(defun svexlist-evals-equal (x env1 env2)
  (declare (xargs :guard (and (svexlist-p x)
                              (svex-env-p env1)
                              (svex-env-p env2))))
  (let ((__function__ 'svexlist-evals-equal))
    (declare (ignorable __function__))
    (equal (svexlist-eval x env1)
           (svexlist-eval x env2))))