		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-collect-modules-from-descriptions

Signature
(vl-collect-modules-from-descriptions x) → mods
Arguments: x — Guard (vl-descriptionlist-p x).
Returns: mods — Type (vl-modulelist-p mods).

Definitions and Theorems

Function: vl-collect-modules-from-descriptions

(defun
  vl-collect-modules-from-descriptions (x)
  (declare (xargs :guard (vl-descriptionlist-p x)))
  (let ((__function__ 'vl-collect-modules-from-descriptions))
       (declare (ignorable __function__))
       (b* (((when (atom x)) nil)
            (x1 (vl-description-fix (car x)))
            ((when (eq (tag x1) :vl-module))
             (cons x1
                   (vl-collect-modules-from-descriptions (cdr x)))))
           (vl-collect-modules-from-descriptions (cdr x)))))

Theorem: vl-modulelist-p-of-vl-collect-modules-from-descriptions

(defthm vl-modulelist-p-of-vl-collect-modules-from-descriptions
        (b* ((mods (vl-collect-modules-from-descriptions x)))
            (vl-modulelist-p mods))
        :rule-classes :rewrite)