		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Irecursivep

List of mutually recursive functions of which the specified named function is a member, based on the defun form that introduced this function, or nil if the specified function is not recursive.

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

This is a specialization of recursivep with nil as the second argument: the i that starts the name of irecursivep conveys that the result is based on the defun form that introduced fn.

See irecursivep+ for an enhanced variant of this utility.

Definitions and Theorems

Function: irecursivep

(defun irecursivep (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'irecursivep))
    (declare (ignorable __function__))
    (recursivep fn nil wrld)))