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