Eliminate parameters from a list of functions.
(vl-fundecllist-expand-params x warnings) → (mv okp warnings new-x)
Function:
(defun vl-fundecllist-expand-params (x warnings) (declare (xargs :guard (and (vl-fundecllist-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-fundecllist-expand-params)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil)) ((mv car-successp warnings car-prime) (vl-fundecl-expand-params (car x) warnings)) ((mv cdr-successp warnings cdr-prime) (vl-fundecllist-expand-params (cdr x) warnings))) (mv (and car-successp cdr-successp) warnings (cons car-prime cdr-prime)))))
Theorem:
(defthm booleanp-of-vl-fundecllist-expand-params.okp (b* (((mv ?okp ?warnings ?new-x) (vl-fundecllist-expand-params x warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-fundecllist-expand-params.warnings (b* (((mv ?okp ?warnings ?new-x) (vl-fundecllist-expand-params x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-fundecllist-p-of-vl-fundecllist-expand-params.new-x (b* (((mv ?okp ?warnings ?new-x) (vl-fundecllist-expand-params x warnings))) (vl-fundecllist-p new-x)) :rule-classes :rewrite)