		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-lookup-ord-file-scope

Look up an ordinary identifier in the file scope of a validation table.

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

Unlike valid-lookup-ord, this skips any block scopes, and directly looks up the identifier in the file scope. It is used in some situations.

Definitions and Theorems

Function: valid-lookup-ord-file-scope

(defun valid-lookup-ord-file-scope (ident table)
  (declare (xargs :guard (and (identp ident)
                              (valid-tablep table))))
  (let ((__function__ 'valid-lookup-ord-file-scope))
    (declare (ignorable __function__))
    (b* ((scopes (valid-table->scopes table))
         ((when (endp scopes))
          (raise "Internal error: no scopes."))
         (scope (car (last scopes)))
         (ident+info (assoc-equal (ident-fix ident)
                                  (valid-scope->ord scope)))
         ((when ident+info) (cdr ident+info)))
      nil)))

Theorem: valid-ord-info-optionp-of-valid-lookup-ord-file-scope

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

Theorem: valid-lookup-ord-file-scope-of-ident-fix-ident

(defthm valid-lookup-ord-file-scope-of-ident-fix-ident
  (equal (valid-lookup-ord-file-scope (ident-fix ident)
                                      table)
         (valid-lookup-ord-file-scope ident table)))

Theorem: valid-lookup-ord-file-scope-ident-equiv-congruence-on-ident

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

Theorem: valid-lookup-ord-file-scope-of-valid-table-fix-table

(defthm valid-lookup-ord-file-scope-of-valid-table-fix-table
  (equal (valid-lookup-ord-file-scope ident (valid-table-fix table))
         (valid-lookup-ord-file-scope ident table)))

Theorem: valid-lookup-ord-file-scope-valid-table-equiv-congruence-on-table

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