		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Recursivep

Recognizes directly or mutually recursive functions.

Signature
(recursivep ident call-graph) → *
Arguments: ident — Guard (identp ident).; call-graph — Guard (ident-ident-option-set-mapp call-graph).

This function checks whether ident is in its own transitive closure. See call-graph-transitive-closure and (see call-graph).

Definitions and Theorems

Function: recursivep

(defun recursivep (ident call-graph)
 (declare
      (xargs :guard (and (identp ident)
                         (ident-ident-option-set-mapp call-graph))))
 (let ((__function__ 'recursivep))
   (declare (ignorable __function__))
   (exists-call-pathp ident ident call-graph)))