Retrieve the ATJ function type information of the specified function from the table.
(atj-get-function-type-info-from-table fn wrld) → fn-info?
If the table has no entry for the function,
Function:
(defun atj-get-function-type-info-from-table (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'atj-get-function-type-info-from-table)) (declare (ignorable __function__)) (b* ((table (table-alist+ *atj-function-type-info-table-name* wrld) ) (pair (assoc-eq fn table)) ((when pair) (b* ((fn-info (cdr pair))) (if (atj-function-type-info-p fn-info) fn-info (raise "Internal error: ~ malformed function information ~x0 for function ~x1." fn-info fn))))) nil)))
Theorem:
(defthm atj-maybe-function-type-info-p-of-atj-get-function-type-info-from-table (b* ((fn-info? (atj-get-function-type-info-from-table fn wrld))) (atj-maybe-function-type-info-p fn-info?)) :rule-classes :rewrite)
Theorem:
(defthm atj-function-type-info-p-of-atj-get-function-type-info-from-table (iff (atj-function-type-info-p (atj-get-function-type-info-from-table fn wrld)) (atj-get-function-type-info-from-table fn wrld)))