Collect just the interface ports for a genblob.
(vl-genblob->ifports x) → ports
Function:
(defun vl-genblob->ifports (x) (declare (xargs :guard (vl-genblob-p x))) (let ((__function__ 'vl-genblob->ifports)) (declare (ignorable __function__)) (vl-collect-interface-ports (vl-genblob->ports x))))
Theorem:
(defthm vl-interfaceportlist-p-of-vl-genblob->ifports (b* ((ports (vl-genblob->ifports x))) (vl-interfaceportlist-p ports)) :rule-classes :rewrite)
Theorem:
(defthm vl-regularportlist-p-when-no-genblob->ifports (implies (not (vl-genblob->ifports x)) (vl-regularportlist-p (vl-genblob->ports x))))
Theorem:
(defthm vl-genblob->ifports-of-vl-genblob-fix-x (equal (vl-genblob->ifports (vl-genblob-fix x)) (vl-genblob->ifports x)))
Theorem:
(defthm vl-genblob->ifports-vl-genblob-equiv-congruence-on-x (implies (vl-genblob-equiv x x-equiv) (equal (vl-genblob->ifports x) (vl-genblob->ifports x-equiv))) :rule-classes :congruence)