(vl-modulelist-default-signatures names ss warnings) → (mv sigs warnings)
Function:
(defun vl-modulelist-default-signatures (names ss warnings) (declare (xargs :guard (and (string-listp names) (vl-scopestack-p ss) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-modulelist-default-signatures)) (declare (ignorable __function__)) (if (atom names) (mv nil (vl-warninglist-fix warnings)) (b* (((mv sig sig-ss warnings) (vl-module-default-signature (car names) ss warnings)) ((mv sigs warnings) (vl-modulelist-default-signatures (cdr names) ss warnings))) (mv (if sig (cons (cons sig sig-ss) sigs) sigs) warnings)))))
Theorem:
(defthm vl-unparam-sigalist-p-of-vl-modulelist-default-signatures.sigs (b* (((mv ?sigs ?warnings) (vl-modulelist-default-signatures names ss warnings))) (vl-unparam-sigalist-p sigs)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-modulelist-default-signatures.warnings (b* (((mv ?sigs ?warnings) (vl-modulelist-default-signatures names ss warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-default-signatures-of-string-list-fix-names (equal (vl-modulelist-default-signatures (string-list-fix names) ss warnings) (vl-modulelist-default-signatures names ss warnings)))
Theorem:
(defthm vl-modulelist-default-signatures-string-list-equiv-congruence-on-names (implies (str::string-list-equiv names names-equiv) (equal (vl-modulelist-default-signatures names ss warnings) (vl-modulelist-default-signatures names-equiv ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-modulelist-default-signatures-of-vl-scopestack-fix-ss (equal (vl-modulelist-default-signatures names (vl-scopestack-fix ss) warnings) (vl-modulelist-default-signatures names ss warnings)))
Theorem:
(defthm vl-modulelist-default-signatures-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-modulelist-default-signatures names ss warnings) (vl-modulelist-default-signatures names ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-modulelist-default-signatures-of-vl-warninglist-fix-warnings (equal (vl-modulelist-default-signatures names ss (vl-warninglist-fix warnings)) (vl-modulelist-default-signatures names ss warnings)))
Theorem:
(defthm vl-modulelist-default-signatures-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-modulelist-default-signatures names ss warnings) (vl-modulelist-default-signatures names ss warnings-equiv))) :rule-classes :congruence)