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!
(vl-vardecllist-impexp-names decls implicit explicit) → (mv implicit explicit)
Function:
(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:
(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:
(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)