		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Irecursivep+

Enhanced variant of irecursivep.

Signature
(irecursivep+ fn wrld) → clique
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: clique — Type (symbol-listp clique).

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 wrld. Furthermore, this utility causes an error if called on a symbol that does not name a logic-mode function; the reason for ensuring logic mode is that this utility looks at the recursivep property, which is always nil for program-mode functions (i.e. it is set only for logic-mode functions).

Definitions and Theorems

Function: irecursivep+

(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)))))))

Theorem: symbol-listp-of-irecursivep+

(defthm symbol-listp-of-irecursivep+
  (b* ((clique (irecursivep+ fn wrld)))
    (symbol-listp clique))
  :rule-classes :rewrite)