		Search-engine friendly clone of the ACL2 documentation.

Atc-table

Atc-table-lookup

Look up an atc call in the table.

Signature
(atc-table-lookup call wrld) → info?
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: info? — Type (atc-maybe-call-infop info?).

Definitions and Theorems

Function: atc-table-lookup

(defun atc-table-lookup (call wrld)
 (declare (xargs :guard (and (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-table-lookup))
  (declare (ignorable __function__))
  (b* ((table (table-alist+ *atc-table* wrld))
       (info? (cdr (assoc-equal call table))))
   (if (atc-maybe-call-infop info?)
       info?
    (raise
     "Internal error: malformed value ~x0 of key ~x1 in the ATC table."
     info? call)))))

Theorem: atc-maybe-call-infop-of-atc-table-lookup

(defthm atc-maybe-call-infop-of-atc-table-lookup
  (b* ((info? (atc-table-lookup call wrld)))
    (atc-maybe-call-infop info?))
  :rule-classes :rewrite)