(vl-ansi-portdecllist-condcheck! x) → warnings
Function:
(defun vl-ansi-portdecllist-condcheck! (x) (declare (xargs :guard (vl-ansi-portdecllist-p x))) (let ((__function__ 'vl-ansi-portdecllist-condcheck!)) (declare (ignorable __function__)) (b* (((when (atom x)) (b* ((warnings nil)) warnings)) (warnings (vl-ansi-portdecl-condcheck! (car x))) (warnings1 (vl-ansi-portdecllist-condcheck! (cdr x))) (warnings (vl-warningtree-cons warnings1 warnings))) warnings)))
Theorem:
(defthm vl-warningtree-p-of-vl-ansi-portdecllist-condcheck! (b* ((warnings (vl-ansi-portdecllist-condcheck! x))) (vl-warningtree-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-ansi-portdecllist-condcheck!-of-vl-ansi-portdecllist-fix-x (equal (vl-ansi-portdecllist-condcheck! (vl-ansi-portdecllist-fix x)) (vl-ansi-portdecllist-condcheck! x)))
Theorem:
(defthm vl-ansi-portdecllist-condcheck!-vl-ansi-portdecllist-equiv-congruence-on-x (implies (vl-ansi-portdecllist-equiv x x-equiv) (equal (vl-ansi-portdecllist-condcheck! x) (vl-ansi-portdecllist-condcheck! x-equiv))) :rule-classes :congruence)