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