		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-portdecls

Vl-fast-reorder-portdecl

Fast-alist enhanced version of vl-reorder-portdecls.

Signature
(vl-fast-reorder-portdecl names x fal) → *
Arguments: names — Guard (string-listp names).; x — Guard (vl-portdecllist-p x).; fal — Guard (equal fal (vl-portdecllist-alist x nil)).

Definitions and Theorems

Function: vl-fast-reorder-portdecl

(defun vl-fast-reorder-portdecl (names x fal)
 (declare
     (xargs :guard (and (string-listp names)
                        (vl-portdecllist-p x)
                        (equal fal (vl-portdecllist-alist x nil)))))
 (let ((__function__ 'vl-fast-reorder-portdecl))
   (declare (ignorable __function__))
   (b* (((when (atom names)) nil)
        (look (hons-get (car names) fal))
        ((when look)
         (cons (cdr look)
               (vl-fast-reorder-portdecl (cdr names)
                                         x fal))))
     (vl-fast-reorder-portdecl (cdr names)
                               x fal))))