		Search-engine friendly clone of the ACL2 documentation.

Patterns

Subsetp-of-pat-flatten

(subsetp-of-pat-flatten x pat) is an optimized way to ask if x is a subset of (pat-flatten1 pat).

This just avoids flattening the pattern. Don't expect it to be super fast; it's still O(n^2).

Definitions and Theorems

Function: subsetp-of-pat-flatten

(defun subsetp-of-pat-flatten (x pat)
       (declare (xargs :guard t))
       (mbe :logic (subsetp-equal x (pat-flatten1 pat))
            :exec (if (atom x)
                      t
                      (and (member-of-pat-flatten (car x) pat)
                           (subsetp-of-pat-flatten (cdr x) pat)))))