Enhanced variant of table-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
(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)))))
(defthm alistp-of-table-alist+ (b* ((alist (table-alist+ name wrld))) (alistp alist)) :rule-classes :rewrite)