Disambiguate a list of initializer declarators.
(dimb-initdeclor-list ideclors kind table) → (mv erp new-ideclors new-table)
We process each one, in order. The kind is the same for all of them, obtained from the enclosing declaration, and passed to this function as input.
Function:
(defun dimb-initdeclor-list (ideclors kind table) (declare (xargs :guard (and (initdeclor-listp ideclors) (dimb-kindp kind) (dimb-tablep table)))) (let ((__function__ 'dimb-initdeclor-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp ideclors)) (retok nil (dimb-table-fix table))) ((erp new-ideclor table) (dimb-initdeclor (car ideclors) kind table)) ((erp new-ideclors table) (dimb-initdeclor-list (cdr ideclors) kind table))) (retok (cons new-ideclor new-ideclors) table))))
Theorem:
(defthm initdeclor-listp-of-dimb-initdeclor-list.new-ideclors (b* (((mv acl2::?erp ?new-ideclors ?new-table) (dimb-initdeclor-list ideclors kind table))) (initdeclor-listp new-ideclors)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-initdeclor-list.new-table (b* (((mv acl2::?erp ?new-ideclors ?new-table) (dimb-initdeclor-list ideclors kind table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm initdeclor-list-unambp-of-dimb-initdeclor-list (b* (((mv acl2::?erp ?new-ideclors ?new-table) (dimb-initdeclor-list ideclors kind table))) (implies (not erp) (initdeclor-list-unambp new-ideclors))))
Theorem:
(defthm dimb-initdeclor-list-of-initdeclor-list-fix-ideclors (equal (dimb-initdeclor-list (initdeclor-list-fix ideclors) kind table) (dimb-initdeclor-list ideclors kind table)))
Theorem:
(defthm dimb-initdeclor-list-initdeclor-list-equiv-congruence-on-ideclors (implies (initdeclor-list-equiv ideclors ideclors-equiv) (equal (dimb-initdeclor-list ideclors kind table) (dimb-initdeclor-list ideclors-equiv kind table))) :rule-classes :congruence)
Theorem:
(defthm dimb-initdeclor-list-of-dimb-kind-fix-kind (equal (dimb-initdeclor-list ideclors (dimb-kind-fix kind) table) (dimb-initdeclor-list ideclors kind table)))
Theorem:
(defthm dimb-initdeclor-list-dimb-kind-equiv-congruence-on-kind (implies (dimb-kind-equiv kind kind-equiv) (equal (dimb-initdeclor-list ideclors kind table) (dimb-initdeclor-list ideclors kind-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-initdeclor-list-of-dimb-table-fix-table (equal (dimb-initdeclor-list ideclors kind (dimb-table-fix table)) (dimb-initdeclor-list ideclors kind table)))
Theorem:
(defthm dimb-initdeclor-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-initdeclor-list ideclors kind table) (dimb-initdeclor-list ideclors kind table-equiv))) :rule-classes :congruence)