		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-extdecl

Disambiguate an external declaration.

Signature
(dimb-extdecl extdecl table) → (mv erp new-extdecl new-table)
Arguments: extdecl — Guard (extdeclp extdecl).; table — Guard (dimb-tablep table).
Returns: new-extdecl — Type (extdeclp new-extdecl).; new-table — Type (dimb-tablep new-table).

Definitions and Theorems

Function: dimb-extdecl

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

Theorem: extdeclp-of-dimb-extdecl.new-extdecl

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

Theorem: dimb-tablep-of-dimb-extdecl.new-table

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

Theorem: extdecl-unambp-of-dimb-extdecl

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

Theorem: dimb-extdecl-of-extdecl-fix-extdecl

(defthm dimb-extdecl-of-extdecl-fix-extdecl
  (equal (dimb-extdecl (extdecl-fix extdecl)
                       table)
         (dimb-extdecl extdecl table)))

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

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

Theorem: dimb-extdecl-of-dimb-table-fix-table

(defthm dimb-extdecl-of-dimb-table-fix-table
  (equal (dimb-extdecl extdecl (dimb-table-fix table))
         (dimb-extdecl extdecl table)))

Theorem: dimb-extdecl-dimb-table-equiv-congruence-on-table

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