(vl-fundecl-condcheck!-aux x) → warnings
Function:
(defun vl-fundecl-condcheck!-aux (x) (declare (xargs :guard (vl-fundecl-p x))) (let ((__function__ 'vl-fundecl-condcheck!-aux)) (declare (ignorable __function__)) (b* (((vl-fundecl x) (vl-fundecl-fix x))) (b* ((warnings ((lambda (x) (vl-datatype-condcheck x nil)) x.rettype)) (warnings1 ((lambda (x) (vl-stmt-condcheck x nil)) x.body)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-portdecllist-condcheck x nil)) x.portdecls)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 (vl-function-specialization-map-condcheck! x.function-map)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-vardecllist-condcheck x nil)) x.vardecls)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-paramdecllist-condcheck x nil)) x.paramdecls)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-typedeflist-condcheck x nil)) x.typedefs)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-importlist-condcheck x nil)) x.imports)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-atts-condcheck x nil)) x.atts)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 (vl-portdecl-or-blockitem-list-condcheck! x.loaditems)) (warnings (vl-warningtree-cons warnings1 warnings))) warnings))))
Theorem:
(defthm vl-warningtree-p-of-vl-fundecl-condcheck!-aux (b* ((warnings (vl-fundecl-condcheck!-aux x))) (vl-warningtree-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-fundecl-condcheck!-aux-of-vl-fundecl-fix-x (equal (vl-fundecl-condcheck!-aux (vl-fundecl-fix x)) (vl-fundecl-condcheck!-aux x)))
Theorem:
(defthm vl-fundecl-condcheck!-aux-vl-fundecl-equiv-congruence-on-x (implies (vl-fundecl-equiv x x-equiv) (equal (vl-fundecl-condcheck!-aux x) (vl-fundecl-condcheck!-aux x-equiv))) :rule-classes :congruence)