(vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings) → (mv okp warnings nf vacc aacc ports portdecls vardecls paramdecls)
Function:
(defun vl-module-expand-calls-in-decls (ports portdecls vardecls paramdecls ss nf vacc aacc warnings) (declare (xargs :guard (and (vl-portlist-p ports) (vl-portdecllist-p portdecls) (vl-vardecllist-p vardecls) (vl-paramdecllist-p paramdecls) (vl-scopestack-p ss) (vl-namefactory-p nf) (vl-vardecllist-p vacc) (vl-assignlist-p aacc) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-module-expand-calls-in-decls)) (declare (ignorable __function__)) (b* (((mv okp1 warnings nf ports vacc aacc) (vl-portlist-expand-function-calls ports ss nf vacc aacc warnings)) ((mv okp2 warnings nf portdecls vacc aacc) (vl-portdecllist-expand-function-calls portdecls ss nf vacc aacc warnings)) ((mv okp3 warnings nf vardecls vacc aacc) (vl-vardecllist-expand-function-calls vardecls ss nf vacc aacc warnings)) ((mv okp4 warnings nf paramdecls vacc aacc) (vl-paramdecllist-expand-function-calls paramdecls ss nf vacc aacc warnings))) (mv (and* okp1 okp2 okp3 okp4) warnings nf vacc aacc ports portdecls vardecls paramdecls))))
Theorem:
(defthm booleanp-of-vl-module-expand-calls-in-decls.okp (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-module-expand-calls-in-decls.warnings (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-module-expand-calls-in-decls.nf (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-module-expand-calls-in-decls.vacc (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-vardecllist-p vacc)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-module-expand-calls-in-decls.aacc (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-assignlist-p aacc)) :rule-classes :rewrite)
Theorem:
(defthm vl-portlist-p-of-vl-module-expand-calls-in-decls.ports (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-portlist-p ports)) :rule-classes :rewrite)
Theorem:
(defthm vl-portdecllist-p-of-vl-module-expand-calls-in-decls.portdecls (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-module-expand-calls-in-decls.vardecls (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-module-expand-calls-in-decls.paramdecls (b* (((mv ?okp ?warnings ?nf ?vacc ?aacc ?ports ?portdecls ?vardecls ?paramdecls) (vl-module-expand-calls-in-decls ports portdecls vardecls paramdecls ss nf vacc aacc warnings))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)