Enhanced variant of irecursivep.
This returns the same result as irecursivep,
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 irecursivep+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'irecursivep+)) (declare (ignorable __function__)) (cond ((not (function-symbolp fn wrld)) (raise "The symbol ~x0 does not name a function." fn)) ((not (logicp fn wrld)) (raise "The function ~x0 is not in logic mode." fn)) (t (b* ((result (irecursivep fn wrld))) (if (symbol-listp result) result (raise "Internal error: ~ the RECURSIVEP property ~x0 of ~x1 ~ is not a true list of symbols." result fn)))))))
(defthm symbol-listp-of-irecursivep+ (b* ((clique (irecursivep+ fn wrld))) (symbol-listp clique)) :rule-classes :rewrite)