		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-ext-declon-list

Disambiguate a list of external declarations.

Signature
(dimb-ext-declon-list edecls table gcc) → (mv erp new-edecls new-table)
Arguments: edecls — Guard (ext-declon-listp edecls).; table — Guard (dimb-tablep table).; gcc — Guard (booleanp gcc).
Returns: erp — Type (maybe-msgp erp).; new-edecls — Type (ext-declon-listp new-edecls).; new-table — Type (dimb-tablep new-table).

Definitions and Theorems

Function: dimb-ext-declon-list

(defun dimb-ext-declon-list (edecls table gcc)
  (declare (xargs :guard (and (ext-declon-listp edecls)
                              (dimb-tablep table)
                              (booleanp gcc))))
  (let ((__function__ 'dimb-ext-declon-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil (irr-dimb-table))
         ((when (endp edecls))
          (retok nil (dimb-table-fix table)))
         ((erp new-edecl table)
          (dimb-ext-declon (car edecls)
                           table gcc))
         ((erp new-edecls table)
          (dimb-ext-declon-list (cdr edecls)
                                table gcc)))
      (retok (cons new-edecl new-edecls)
             table))))

Theorem: maybe-msgp-of-dimb-ext-declon-list.erp

(defthm maybe-msgp-of-dimb-ext-declon-list.erp
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (dimb-ext-declon-list edecls table gcc)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: ext-declon-listp-of-dimb-ext-declon-list.new-edecls

(defthm ext-declon-listp-of-dimb-ext-declon-list.new-edecls
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (dimb-ext-declon-list edecls table gcc)))
    (ext-declon-listp new-edecls))
  :rule-classes :rewrite)

Theorem: dimb-tablep-of-dimb-ext-declon-list.new-table

(defthm dimb-tablep-of-dimb-ext-declon-list.new-table
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (dimb-ext-declon-list edecls table gcc)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: ext-declon-list-unambp-of-dimb-ext-declon-list

(defthm ext-declon-list-unambp-of-dimb-ext-declon-list
  (b* (((mv acl2::?erp ?new-edecls ?new-table)
        (dimb-ext-declon-list edecls table gcc)))
    (implies (not erp)
             (ext-declon-list-unambp new-edecls))))

Theorem: dimb-ext-declon-list-of-ext-declon-list-fix-edecls

(defthm dimb-ext-declon-list-of-ext-declon-list-fix-edecls
  (equal (dimb-ext-declon-list (ext-declon-list-fix edecls)
                               table gcc)
         (dimb-ext-declon-list edecls table gcc)))

Theorem: dimb-ext-declon-list-ext-declon-list-equiv-congruence-on-edecls

(defthm
    dimb-ext-declon-list-ext-declon-list-equiv-congruence-on-edecls
  (implies (ext-declon-list-equiv edecls edecls-equiv)
           (equal (dimb-ext-declon-list edecls table gcc)
                  (dimb-ext-declon-list edecls-equiv table gcc)))
  :rule-classes :congruence)

Theorem: dimb-ext-declon-list-of-dimb-table-fix-table

(defthm dimb-ext-declon-list-of-dimb-table-fix-table
  (equal (dimb-ext-declon-list edecls (dimb-table-fix table)
                               gcc)
         (dimb-ext-declon-list edecls table gcc)))

Theorem: dimb-ext-declon-list-dimb-table-equiv-congruence-on-table

(defthm dimb-ext-declon-list-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-ext-declon-list edecls table gcc)
                  (dimb-ext-declon-list edecls table-equiv gcc)))
  :rule-classes :congruence)

Theorem: dimb-ext-declon-list-of-bool-fix-gcc

(defthm dimb-ext-declon-list-of-bool-fix-gcc
  (equal (dimb-ext-declon-list edecls table (bool-fix gcc))
         (dimb-ext-declon-list edecls table gcc)))

Theorem: dimb-ext-declon-list-iff-congruence-on-gcc

(defthm dimb-ext-declon-list-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (dimb-ext-declon-list edecls table gcc)
                  (dimb-ext-declon-list edecls table gcc-equiv)))
  :rule-classes :congruence)