		Search-engine friendly clone of the ACL2 documentation.

Patterns

Data-for-patternp

(data-for-patternp pat data) determines whether data is compatible with the pattern pat.

Definitions and Theorems

Function: data-for-patternp

(defun data-for-patternp (pat data)
       (declare (xargs :guard t))
       (if pat
           (or (atom pat)
               (and (consp data)
                    (data-for-patternp (car pat) (car data))
                    (data-for-patternp (cdr pat)
                                       (cdr data))))
           t))