Obtain the ATJ function type information of the specified function.
(atj-get-function-type-info fn guards$ wrld) → fn-info
If the
Function:
(defun atj-get-function-type-info (fn guards$ wrld) (declare (xargs :guard (and (symbolp fn) (booleanp guards$) (plist-worldp wrld)))) (let ((__function__ 'atj-get-function-type-info)) (declare (ignorable __function__)) (if guards$ (b* ((fn-info? (atj-get-function-type-info-from-table fn wrld))) (or fn-info? (atj-function-type-info-default fn wrld))) (atj-function-type-info-default fn wrld))))
Theorem:
(defthm atj-function-type-info-p-of-atj-get-function-type-info (b* ((fn-info (atj-get-function-type-info fn guards$ wrld))) (atj-function-type-info-p fn-info)) :rule-classes :rewrite)