		Search-engine friendly clone of the ACL2 documentation.

Patterns

Pat->fal

Alternative to pat->al that generates a fast alist.

The input al also needs to be fast.

Definitions and Theorems

Function: pat->fal

(defun
   pat->fal (pat data al)
   (declare (xargs :guard (data-for-patternp pat data)))
   (mbe :logic (pat->al pat data al)
        :exec (if pat
                  (if (atom pat)
                      (hons-acons pat data al)
                      (pat->fal (car pat)
                                (car data)
                                (pat->fal (cdr pat) (cdr data) al)))
                  al)))