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