		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-vars

4v-sexpr-vars-1pass-list

Often faster alternative to 4v-sexpr-vars-list.

This uses the 4v-sexpr-vars-1pass strategy to gather variables from a list of sexprs.

Definitions and Theorems

Function: 4v-sexpr-vars-1pass-list

(defun 4v-sexpr-vars-1pass-list (x)
  (declare (xargs :guard t))
  (mbe :logic (4v-sexpr-vars-list x)
       :exec
       (b* (((mv seen vars)
             (4v-sexpr-vars-1pass-list-exec x nil nil)))
         (fast-alist-free seen)
         (set::mergesort vars))))