		Search-engine friendly clone of the ACL2 documentation.

Patterns

Assoc-pat->al

(assoc-pat->al key pat data) is an optimized way to look up a particular key, given some pattern and data.

This is logically just a lookup in the alist constructed by pat->al, but we avoid constructing the alist.

Definitions and Theorems

Function: assoc-pat->al

(defun
     assoc-pat->al (key pat data)
     (declare (xargs :guard (data-for-patternp pat data)))
     (mbe :logic (hons-assoc-equal key (pat->al pat data nil))
          :exec (if pat
                    (if (atom pat)
                        (if (equal key pat) (cons pat data) nil)
                        (or (assoc-pat->al key (car pat) (car data))
                            (assoc-pat->al key (cdr pat)
                                           (cdr data))))
                    nil)))