		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-ext-declon

Disambiguate an external declaration.

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

Definitions and Theorems

Function: dimb-ext-declon

(defun dimb-ext-declon (extdecl table gcc)
 (declare (xargs :guard (and (ext-declonp extdecl)
                             (dimb-tablep table)
                             (booleanp gcc))))
 (let ((__function__ 'dimb-ext-declon))
   (declare (ignorable __function__))
   (b* (((reterr)
         (irr-ext-declon)
         (irr-dimb-table)))
     (ext-declon-case extdecl :fundef
                      (b* (((erp new-fundef table)
                            (dimb-fundef extdecl.fundef table gcc)))
                        (retok (ext-declon-fundef new-fundef)
                               table))
                      :declon
                      (b* (((erp new-decl table)
                            (dimb-declon extdecl.declon table)))
                        (retok (ext-declon-declon new-decl)
                               table))
                      :empty (retok (ext-declon-fix extdecl)
                                    (dimb-table-fix table))
                      :asm (retok (ext-declon-fix extdecl)
                                  (dimb-table-fix table))))))

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

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

Theorem: ext-declonp-of-dimb-ext-declon.new-extdecl

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

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

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

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

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

Theorem: dimb-ext-declon-of-ext-declon-fix-extdecl

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

Theorem: dimb-ext-declon-ext-declon-equiv-congruence-on-extdecl

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

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

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

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

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

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

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

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

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