Get the ports field from a vl-nonansi-ports.
(vl-nonansi-ports->ports x) → ports
This is an ordinary field accessor created by defprod.
Function:
(defun vl-nonansi-ports->ports$inline (x) (declare (xargs :guard (vl-parsed-ports-p x))) (declare (xargs :guard (equal (vl-parsed-ports-kind x) :nonansi))) (let ((__function__ 'vl-nonansi-ports->ports)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and (equal (vl-parsed-ports-kind x) :nonansi) x))) (vl-portlist-fix (std::da-nth 0 (cdr x)))) :exec (std::da-nth 0 (cdr x)))))
Theorem:
(defthm vl-portlist-p-of-vl-nonansi-ports->ports (b* ((ports (vl-nonansi-ports->ports$inline x))) (vl-portlist-p ports)) :rule-classes :rewrite)
Theorem:
(defthm vl-nonansi-ports->ports$inline-of-vl-parsed-ports-fix-x (equal (vl-nonansi-ports->ports$inline (vl-parsed-ports-fix x)) (vl-nonansi-ports->ports$inline x)))
Theorem:
(defthm vl-nonansi-ports->ports$inline-vl-parsed-ports-equiv-congruence-on-x (implies (vl-parsed-ports-equiv x x-equiv) (equal (vl-nonansi-ports->ports$inline x) (vl-nonansi-ports->ports$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-nonansi-ports->ports-when-wrong-kind (implies (not (equal (vl-parsed-ports-kind x) :nonansi)) (equal (vl-nonansi-ports->ports x) (vl-portlist-fix nil))))