		Search-engine friendly clone of the ACL2 documentation.

Hierarchy

Vl-collect-dependencies

Signature
(vl-collect-dependencies names graph) → dependencies
Arguments: names — Guard (string-listp names).; graph — Guard (and (vl-depgraph-p graph) (depgraph::alist-values-are-sets-p graph)) .
Returns: dependencies — Type (and (string-listp dependencies) (setp dependencies)), given the guard.

Definitions and Theorems

Function: vl-collect-dependencies

(defun vl-collect-dependencies (names graph)
 (declare
  (xargs
      :guard (and (string-listp names)
                  (and (vl-depgraph-p graph)
                       (depgraph::alist-values-are-sets-p graph)))))
 (let ((__function__ 'vl-collect-dependencies))
   (declare (ignorable __function__))
   (if (atom names)
       nil
     (union (cdr (hons-get (car names) graph))
            (vl-collect-dependencies (cdr names)
                                     graph)))))

Theorem: return-type-of-vl-collect-dependencies

(defthm return-type-of-vl-collect-dependencies
 (implies (and (force (string-listp names))
               (force (vl-depgraph-p graph))
               (force (depgraph::alist-values-are-sets-p graph)))
          (b* ((dependencies (vl-collect-dependencies names graph)))
            (and (string-listp dependencies)
                 (setp dependencies))))
 :rule-classes :rewrite)