		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Valid-table-global-lookup

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

Definitions and Theorems

Function: valid-table-global-lookup

(defun valid-table-global-lookup (ident valid-table)
 (declare (xargs :guard (and (identp ident)
                             (c$::valid-tablep valid-table))))
 (let ((__function__ 'valid-table-global-lookup))
  (declare (ignorable __function__))
  (b*
   ((scopes (c$::valid-table->scopes valid-table))
    ((when (endp scopes))
     (raise "Ill-formed validation table: no scope found"))
    ((unless (endp (rest scopes)))
     (raise
          "Ill-formed validation table: more than one scope found"))
    (scope (first scopes))
    (ord (c$::valid-scope->ord scope))
    (lookup (assoc-equal ident ord)))
   (if lookup (cdr lookup) nil))))

Theorem: valid-ord-info-optionp-of-valid-table-global-lookup

(defthm valid-ord-info-optionp-of-valid-table-global-lookup
  (b* ((info? (valid-table-global-lookup ident valid-table)))
    (c$::valid-ord-info-optionp info?))
  :rule-classes :rewrite)