		Search-engine friendly clone of the ACL2 documentation.

Patterns

Pat-flatten

Flatten a pattern into a list of atoms (with an accumulator).

(pat-flatten pat acc) flattens pat, appending its atoms onto acc, in order. For instance,

(pat-flatten '((a) (b c)) '(x y z))
-->
(a b c x y z)

The accumulator argument is occasionally useful. But for reasoning, we rewrite pat-flatten into pat-flatten1 with the following theorem:

Theorem: pat-flatten-is-pat-flatten1

(defthm pat-flatten-is-pat-flatten1
        (equal (pat-flatten pat acc)
               (append (pat-flatten1 pat) acc)))

Definitions and Theorems

Function: pat-flatten

(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))