		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-modules

Vl-slow-reorder-module

Non fast-alist version of vl-reorder-modules, used when the lists are really short.

Signature
(vl-slow-reorder-module names x) → *
Arguments: names — Guard (string-listp names).; x — Guard (vl-modulelist-p x).

You should ordinarily never reason about this because of the following rule, which we leave enabled.

Theorem: vl-slow-reorder-module-removal

(defthm vl-slow-reorder-module-removal
  (equal (vl-slow-reorder-module names x)
         (vl-reorder-modules names x)))

Definitions and Theorems

Function: vl-slow-reorder-module

(defun vl-slow-reorder-module (names x)
  (declare (xargs :guard (and (string-listp names)
                              (vl-modulelist-p x))))
  (let ((__function__ 'vl-slow-reorder-module))
    (declare (ignorable __function__))
    (b* (((when (atom names)) nil)
         (decl (vl-find-module (car names) x))
         ((when decl)
          (cons decl
                (vl-slow-reorder-module (cdr names)
                                        x))))
      (vl-slow-reorder-module (cdr names)
                              x))))