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