		Search-engine friendly clone of the ACL2 documentation.

Std/system

Table-alist+

Enhanced variant of table-alist.

Signature
(table-alist+ name wrld) → alist
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: alist — Type (alistp alist).

This returns the same result as the built-in table-alist function (see the ACL2 system sources), but it includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld.

Definitions and Theorems

Function: table-alist+

(defun table-alist+ (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'table-alist+))
  (declare (ignorable __function__))
  (b* ((result (table-alist name wrld)))
   (if (alistp result)
       result
    (raise
     "Internal error: ~
              the TABLE-ALIST property ~x0 of ~x1 is not an alist."
     result name)))))

Theorem: alistp-of-table-alist+

(defthm alistp-of-table-alist+
  (b* ((alist (table-alist+ name wrld)))
    (alistp alist))
  :rule-classes :rewrite)