(vl-vardecllist->initvals x) → vals
Function:
(defun vl-vardecllist->initvals (x) (declare (xargs :guard (vl-vardecllist-p x))) (let ((__function__ 'vl-vardecllist->initvals)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (initval (vl-vardecl->initval (car x)))) (if initval (cons initval (vl-vardecllist->initvals (cdr x))) (vl-vardecllist->initvals (cdr x))))))
Theorem:
(defthm vl-exprlist-p-of-vl-vardecllist->initvals (b* ((vals (vl-vardecllist->initvals x))) (vl-exprlist-p vals)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist->initvals-of-vl-vardecllist-fix-x (equal (vl-vardecllist->initvals (vl-vardecllist-fix x)) (vl-vardecllist->initvals x)))
Theorem:
(defthm vl-vardecllist->initvals-vl-vardecllist-equiv-congruence-on-x (implies (vl-vardecllist-equiv x x-equiv) (equal (vl-vardecllist->initvals x) (vl-vardecllist->initvals x-equiv))) :rule-classes :congruence)