		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Direct-recursivep

Recognizes functions which calls themselves.

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

This function checks where the ident is related to itself under the call graph. See call-graph-transitive-closure and (see call-graph).

Definitions and Theorems

Function: direct-recursivep

(defun direct-recursivep (ident call-graph)
 (declare
      (xargs :guard (and (identp ident)
                         (ident-ident-option-set-mapp call-graph))))
 (let ((__function__ 'direct-recursivep))
   (declare (ignorable __function__))
   (b* ((lookup (omap::assoc ident call-graph)))
     (and lookup (in ident (cdr lookup))))))