(vl-portdecl-or-blockitem-condcheck! x) → warnings
Function:
(defun vl-portdecl-or-blockitem-condcheck! (x) (declare (xargs :guard (vl-portdecl-or-blockitem-p x))) (let ((__function__ 'vl-portdecl-or-blockitem-condcheck!)) (declare (ignorable __function__)) (let ((x (vl-portdecl-or-blockitem-fix x))) (common-lisp::case (tag x) ((:vl-portdecl) (b* ((warnings ((lambda (x) (vl-portdecl-condcheck x nil)) x))) warnings)) (otherwise (b* ((warnings ((lambda (x) (vl-blockitem-condcheck x nil)) x))) warnings))))))
Theorem:
(defthm vl-warningtree-p-of-vl-portdecl-or-blockitem-condcheck! (b* ((warnings (vl-portdecl-or-blockitem-condcheck! x))) (vl-warningtree-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-portdecl-or-blockitem-condcheck!-of-vl-portdecl-or-blockitem-fix-x (equal (vl-portdecl-or-blockitem-condcheck! (vl-portdecl-or-blockitem-fix x)) (vl-portdecl-or-blockitem-condcheck! x)))
Theorem:
(defthm vl-portdecl-or-blockitem-condcheck!-vl-portdecl-or-blockitem-equiv-congruence-on-x (implies (vl-portdecl-or-blockitem-equiv x x-equiv) (equal (vl-portdecl-or-blockitem-condcheck! x) (vl-portdecl-or-blockitem-condcheck! x-equiv))) :rule-classes :congruence)