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