		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-lookup-ext

Look up the validation information of an identifier in the externals map.

Signature
(valid-lookup-ext ident table) → info?
Arguments: ident — Guard (identp ident).; table — Guard (valid-tablep table).
Returns: info? — Type (valid-ext-info-optionp info?).

This holds the validation information for an identifier with external linkage which has been declared in any scope or translation unit. See valid-table.

Definitions and Theorems

Function: valid-lookup-ext

(defun valid-lookup-ext (ident table)
  (declare (xargs :guard (and (identp ident)
                              (valid-tablep table))))
  (b* (((valid-table table) table))
    (cdr (omap::assoc (ident-fix ident)
                      table.externals))))

Theorem: valid-ext-info-optionp-of-valid-lookup-ext

(defthm valid-ext-info-optionp-of-valid-lookup-ext
  (b* ((info? (valid-lookup-ext ident table)))
    (valid-ext-info-optionp info?))
  :rule-classes :rewrite)

Theorem: valid-lookup-ext-of-ident-fix-ident

(defthm valid-lookup-ext-of-ident-fix-ident
  (equal (valid-lookup-ext (ident-fix ident)
                           table)
         (valid-lookup-ext ident table)))

Theorem: valid-lookup-ext-ident-equiv-congruence-on-ident

(defthm valid-lookup-ext-ident-equiv-congruence-on-ident
  (implies (ident-equiv ident ident-equiv)
           (equal (valid-lookup-ext ident table)
                  (valid-lookup-ext ident-equiv table)))
  :rule-classes :congruence)

Theorem: valid-lookup-ext-of-valid-table-fix-table

(defthm valid-lookup-ext-of-valid-table-fix-table
  (equal (valid-lookup-ext ident (valid-table-fix table))
         (valid-lookup-ext ident table)))

Theorem: valid-lookup-ext-valid-table-equiv-congruence-on-table

(defthm valid-lookup-ext-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-lookup-ext ident table)
                  (valid-lookup-ext ident table-equiv)))
  :rule-classes :congruence)