		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-modules

Vl-fast-reorder-module

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

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

Definitions and Theorems

Function: vl-fast-reorder-module

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