Collect up a vl-exprctxalist-p from a list of vl-portdecllist-ps.
(vl-portdecllist-ctxexprs mod x) → alist
Function:
(defun vl-portdecllist-ctxexprs (mod x) (declare (xargs :guard (and (stringp mod) (vl-portdecllist-p x)))) (let ((__function__ 'vl-portdecllist-ctxexprs)) (declare (ignorable __function__)) (mbe :logic (if (atom x) nil (append (vl-portdecl-ctxexprs mod (car x)) (vl-portdecllist-ctxexprs mod (cdr x)))) :exec (with-local-nrev (vl-portdecllist-ctxexprs-nrev mod x nrev)))))
Theorem:
(defthm vl-exprctxalist-p-of-vl-portdecllist-ctxexprs (b* ((alist (vl-portdecllist-ctxexprs mod x))) (vl-exprctxalist-p alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-portdecllist-ctxexprs-nrev-removal (equal (vl-portdecllist-ctxexprs-nrev mod x nrev) (append nrev (vl-portdecllist-ctxexprs mod x))))
Theorem:
(defthm vl-portdecllist-ctxexprs-of-str-fix-mod (equal (vl-portdecllist-ctxexprs (str-fix mod) x) (vl-portdecllist-ctxexprs mod x)))
Theorem:
(defthm vl-portdecllist-ctxexprs-streqv-congruence-on-mod (implies (streqv mod mod-equiv) (equal (vl-portdecllist-ctxexprs mod x) (vl-portdecllist-ctxexprs mod-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-portdecllist-ctxexprs-of-vl-portdecllist-fix-x (equal (vl-portdecllist-ctxexprs mod (vl-portdecllist-fix x)) (vl-portdecllist-ctxexprs mod x)))
Theorem:
(defthm vl-portdecllist-ctxexprs-vl-portdecllist-equiv-congruence-on-x (implies (vl-portdecllist-equiv x x-equiv) (equal (vl-portdecllist-ctxexprs mod x) (vl-portdecllist-ctxexprs mod x-equiv))) :rule-classes :congruence)