Flatten a pattern into a list of atoms (with an accumulator).
(pat-flatten pat acc) flattens
(pat-flatten '((a) (b c)) '(x y z)) --> (a b c x y z)
The accumulator argument is occasionally useful. But for reasoning, we
(defthm pat-flatten-is-pat-flatten1 (equal (pat-flatten pat acc) (append (pat-flatten1 pat) acc)))
(defun pat-flatten (pat acc) (declare (xargs :guard t)) (if pat (if (atom pat) (cons pat acc) (pat-flatten (car pat) (pat-flatten (cdr pat) acc))) acc))