Disambiguate a list of declarations.
(dimb-decl-list decls table) → (mv erp new-decls new-table)
The disambiguation table is threaded through.
Function:
(defun dimb-decl-list (decls table) (declare (xargs :guard (and (decl-listp decls) (dimb-tablep table)))) (let ((__function__ 'dimb-decl-list)) (declare (ignorable __function__)) (b* (((reterr) nil (dimb-table-fix table)) ((when (endp decls)) (retok nil (dimb-table-fix table))) ((erp new-decl table) (dimb-decl (car decls) table)) ((erp new-decls table) (dimb-decl-list (cdr decls) table))) (retok (cons new-decl new-decls) table))))
Theorem:
(defthm decl-listp-of-dimb-decl-list.new-decls (b* (((mv acl2::?erp ?new-decls ?new-table) (dimb-decl-list decls table))) (decl-listp new-decls)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-decl-list.new-table (b* (((mv acl2::?erp ?new-decls ?new-table) (dimb-decl-list decls table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm decl-list-unambp-of-dimb-decl-list (b* (((mv acl2::?erp ?new-decls ?new-table) (dimb-decl-list decls table))) (implies (not erp) (decl-list-unambp new-decls))))
Theorem:
(defthm dimb-decl-list-of-decl-list-fix-decls (equal (dimb-decl-list (decl-list-fix decls) table) (dimb-decl-list decls table)))
Theorem:
(defthm dimb-decl-list-decl-list-equiv-congruence-on-decls (implies (decl-list-equiv decls decls-equiv) (equal (dimb-decl-list decls table) (dimb-decl-list decls-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-decl-list-of-dimb-table-fix-table (equal (dimb-decl-list decls (dimb-table-fix table)) (dimb-decl-list decls table)))
Theorem:
(defthm dimb-decl-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-decl-list decls table) (dimb-decl-list decls table-equiv))) :rule-classes :congruence)