		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)