		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-vars

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

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

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

Definitions and Theorems

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

(defun 4v-sexpr-vars-1pass-list-list-exec (x seen vars)
  (declare (xargs :guard t))
  (b* (((when (atom x)) (mv seen vars))
       ((mv seen vars)
        (4v-sexpr-vars-1pass-list-exec (car x)
                                       seen vars)))
    (4v-sexpr-vars-1pass-list-list-exec (cdr x)
                                        seen vars)))

Theorem: 4v-sexpr-vars-1pass-list-list-exec-correct

(defthm 4v-sexpr-vars-1pass-list-list-exec-correct
  (equal
       (set::mergesort
            (mv-nth 1
                    (4v-sexpr-vars-1pass-list-list-exec x nil nil)))
       (4v-sexpr-vars-list-list x)))

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

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