		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-add-ident-objfun

Add an identifier to the disambiguation table, with object or function kind.

Signature
(dimb-add-ident-objfun ident table) → new-table
Arguments: ident — Guard (identp ident).; table — Guard (dimb-tablep table).
Returns: new-table — Type (dimb-tablep new-table).

Definitions and Theorems

Function: dimb-add-ident-objfun

(defun dimb-add-ident-objfun (ident table)
  (declare (xargs :guard (and (identp ident)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-add-ident-objfun))
    (declare (ignorable __function__))
    (dimb-add-ident ident (dimb-kind-objfun)
                    table)))

Theorem: dimb-tablep-of-dimb-add-ident-objfun

(defthm dimb-tablep-of-dimb-add-ident-objfun
  (b* ((new-table (dimb-add-ident-objfun ident table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: dimb-add-ident-objfun-of-ident-fix-ident

(defthm dimb-add-ident-objfun-of-ident-fix-ident
  (equal (dimb-add-ident-objfun (ident-fix ident)
                                table)
         (dimb-add-ident-objfun ident table)))

Theorem: dimb-add-ident-objfun-ident-equiv-congruence-on-ident

(defthm dimb-add-ident-objfun-ident-equiv-congruence-on-ident
  (implies (ident-equiv ident ident-equiv)
           (equal (dimb-add-ident-objfun ident table)
                  (dimb-add-ident-objfun ident-equiv table)))
  :rule-classes :congruence)

Theorem: dimb-add-ident-objfun-of-dimb-table-fix-table

(defthm dimb-add-ident-objfun-of-dimb-table-fix-table
  (equal (dimb-add-ident-objfun ident (dimb-table-fix table))
         (dimb-add-ident-objfun ident table)))

Theorem: dimb-add-ident-objfun-dimb-table-equiv-congruence-on-table

(defthm dimb-add-ident-objfun-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-add-ident-objfun ident table)
                  (dimb-add-ident-objfun ident table-equiv)))
  :rule-classes :congruence)