Function:
(defun vl-vardecllist-reasonable-p (x) (declare (xargs :guard (vl-vardecllist-p x))) (if (atom x) t (and (vl-vardecl-reasonable-p (car x)) (vl-vardecllist-reasonable-p (cdr x)))))
Function:
(defun vl-vardecllist-reasonable-p-warn (x warnings) (declare (xargs :guard (and (vl-vardecllist-p x) (vl-warninglist-p warnings))) (ignorable warnings)) (if (atom x) (mv t warnings) (b* (((mv __ok1__ warnings) (vl-vardecl-reasonable-p-warn (car x) warnings)) ((mv __ok2__ warnings) (b* (((mv __ok1__ warnings) (vl-vardecllist-reasonable-p-warn (cdr x) warnings)) ((mv __ok2__ warnings) (mv t warnings))) (mv (and __ok1__ __ok2__) warnings)))) (mv (and __ok1__ __ok2__) warnings))))
Theorem:
(defthm eliminate-vl-vardecllist-reasonable-p-warn (equal (mv-nth 0 (vl-vardecllist-reasonable-p-warn x warnings)) (vl-vardecllist-reasonable-p x)))
Theorem:
(defthm vl-warninglist-p-of-vl-vardecllist-reasonable-p-warn (implies (force (vl-warninglist-p warnings)) (vl-warninglist-p (mv-nth 1 (vl-vardecllist-reasonable-p-warn x warnings)))))