(vl-collect-unsized-ints x ss scopes) → sub-x
Function:
(defun vl-collect-unsized-ints (x ss scopes) (declare (xargs :guard (and (vl-exprlist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-collect-unsized-ints)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (x1 (vl-expr-fix (car x))) (keep (vl-is-unsized-int x1 ss scopes))) (if keep (cons x1 (vl-collect-unsized-ints (cdr x) ss scopes)) (vl-collect-unsized-ints (cdr x) ss scopes)))))
Theorem:
(defthm vl-exprlist-p-of-vl-collect-unsized-ints (b* ((sub-x (vl-collect-unsized-ints x ss scopes))) (vl-exprlist-p sub-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-collect-unsized-ints-of-vl-exprlist-fix-x (equal (vl-collect-unsized-ints (vl-exprlist-fix x) ss scopes) (vl-collect-unsized-ints x ss scopes)))
Theorem:
(defthm vl-collect-unsized-ints-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-collect-unsized-ints x ss scopes) (vl-collect-unsized-ints x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-collect-unsized-ints-of-vl-scopestack-fix-ss (equal (vl-collect-unsized-ints x (vl-scopestack-fix ss) scopes) (vl-collect-unsized-ints x ss scopes)))
Theorem:
(defthm vl-collect-unsized-ints-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-collect-unsized-ints x ss scopes) (vl-collect-unsized-ints x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-collect-unsized-ints-of-vl-elabscopes-fix-scopes (equal (vl-collect-unsized-ints x ss (vl-elabscopes-fix scopes)) (vl-collect-unsized-ints x ss scopes)))
Theorem:
(defthm vl-collect-unsized-ints-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-collect-unsized-ints x ss scopes) (vl-collect-unsized-ints x ss scopes-equiv))) :rule-classes :congruence)