		Search-engine friendly clone of the ACL2 documentation.

Svex-vars

Svexlist-collect-vars

Usually faster alternative to svexlist-vars.

Signature
(svexlist-collect-vars x) → vars
Arguments: x — Guard (svexlist-p x).
Returns: vars — Type (svarlist-p vars).

See svex-collect-vars. This is just the extension of its strategy to collect all variables that occur in an expression list. Correctness is stated in terms of svexlist-vars:

Theorem: svexlist-collect-vars-correct

(defthm svexlist-collect-vars-correct
  (set-equiv (svexlist-collect-vars x)
             (svexlist-vars x)))

Definitions and Theorems

Function: svexlist-collect-vars

(defun svexlist-collect-vars (x)
  (declare (xargs :guard (svexlist-p x)))
  (let ((__function__ 'svexlist-collect-vars))
    (declare (ignorable __function__))
    (b* (((mv seen vars)
          (svexlist-collect-vars1 x nil nil)))
      (fast-alist-free seen)
      vars)))

Theorem: svarlist-p-of-svexlist-collect-vars

(defthm svarlist-p-of-svexlist-collect-vars
  (b* ((vars (svexlist-collect-vars x)))
    (svarlist-p vars))
  :rule-classes :rewrite)

Theorem: svexlist-collect-vars-of-svexlist-fix-x

(defthm svexlist-collect-vars-of-svexlist-fix-x
  (equal (svexlist-collect-vars (svexlist-fix x))
         (svexlist-collect-vars x)))

Theorem: svexlist-collect-vars-svexlist-equiv-congruence-on-x

(defthm svexlist-collect-vars-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-collect-vars x)
                  (svexlist-collect-vars x-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-collect-vars-correct

(defthm svexlist-collect-vars-correct
  (set-equiv (svexlist-collect-vars x)
             (svexlist-vars x)))