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