Generate the initial templates for expanding a list of functions.
(vl-fundecllist-expansion-templates x warnings) → (mv okp warnings templates)
See vl-fundecl-expansion-template.
Function:
(defun vl-fundecllist-expansion-templates (x warnings) (declare (xargs :guard (and (vl-fundecllist-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-fundecllist-expansion-templates)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil)) ((mv template1 warnings) (vl-fundecl-expansion-template (car x) warnings)) ((mv cdr-successp warnings cdr-templates) (vl-fundecllist-expansion-templates (cdr x) warnings)) (successp (and template1 cdr-successp)) (templates (and successp (cons template1 cdr-templates)))) (mv successp warnings templates))))
Theorem:
(defthm booleanp-of-vl-fundecllist-expansion-templates.okp (b* (((mv ?okp ?warnings ?templates) (vl-fundecllist-expansion-templates x warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-fundecllist-expansion-templates.warnings (b* (((mv ?okp ?warnings ?templates) (vl-fundecllist-expansion-templates x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-funtemplatelist-p-of-vl-fundecllist-expansion-templates.templates (b* (((mv ?okp ?warnings ?templates) (vl-fundecllist-expansion-templates x warnings))) (vl-funtemplatelist-p templates)) :rule-classes :rewrite)