		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-portdecls

Vl-slow-reorder-portdecl

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

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

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

Theorem: vl-slow-reorder-portdecl-removal

(defthm vl-slow-reorder-portdecl-removal
  (equal (vl-slow-reorder-portdecl names x)
         (vl-reorder-portdecls names x)))

Definitions and Theorems

Function: vl-slow-reorder-portdecl

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