		Search-engine friendly clone of the ACL2 documentation.

Vl-reorder-vardecls

Vl-slow-reorder-vardecl

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

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

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

Theorem: vl-slow-reorder-vardecl-removal

(defthm vl-slow-reorder-vardecl-removal
  (equal (vl-slow-reorder-vardecl names x)
         (vl-reorder-vardecls names x)))

Definitions and Theorems

Function: vl-slow-reorder-vardecl

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