		Search-engine friendly clone of the ACL2 documentation.

Use-set

Vl-vardecllist-impexp-names

Split a list of net declarations into those which are implicit and those which are explicit. Note that this only works if vl-modulelist-make-implicit-wires has been run!

Signature
(vl-vardecllist-impexp-names decls implicit explicit) → (mv implicit explicit)
Arguments: decls — Guard (vl-vardecllist-p decls).
Returns: implicit — Type (string-listp implicit), given (force (string-listp implicit)).; explicit — Type (string-listp explicit), given (force (string-listp explicit)).

Definitions and Theorems

Function: vl-vardecllist-impexp-names

(defun vl-vardecllist-impexp-names (decls implicit explicit)
 (declare (xargs :guard (vl-vardecllist-p decls)))
 (let ((__function__ 'vl-vardecllist-impexp-names))
  (declare (ignorable __function__))
  (b* (((when (atom decls))
        (mv implicit explicit))
       ((vl-vardecl x1)
        (vl-vardecl-fix (car decls)))
       ((when (assoc-equal "VL_IMPLICIT" x1.atts))
        (vl-vardecllist-impexp-names (cdr decls)
                                     (cons x1.name implicit)
                                     explicit)))
   (vl-vardecllist-impexp-names (cdr decls)
                                implicit (cons x1.name explicit)))))

Theorem: string-listp-of-vl-vardecllist-impexp-names.implicit

(defthm string-listp-of-vl-vardecllist-impexp-names.implicit
  (implies
       (force (string-listp implicit))
       (b* (((mv ?implicit ?explicit)
             (vl-vardecllist-impexp-names decls implicit explicit)))
         (string-listp implicit)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-vardecllist-impexp-names.explicit

(defthm string-listp-of-vl-vardecllist-impexp-names.explicit
  (implies
       (force (string-listp explicit))
       (b* (((mv ?implicit ?explicit)
             (vl-vardecllist-impexp-names decls implicit explicit)))
         (string-listp explicit)))
  :rule-classes :rewrite)