		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Topdecl-call-graph

Call graph induced by a top-level declaration.

Signature
(topdecl-call-graph decl) → graph
Arguments: decl — Guard (topdeclp decl).
Returns: graph — Type (alistp graph).

A struct declaration induces no call graph.

Definitions and Theorems

Function: topdecl-call-graph

(defun topdecl-call-graph (decl)
  (declare (xargs :guard (topdeclp decl)))
  (let ((__function__ 'topdecl-call-graph))
    (declare (ignorable __function__))
    (topdecl-case decl
                  :function (fundecl-call-graph decl.get)
                  :struct nil
                  :mapping nil)))

Theorem: alistp-of-topdecl-call-graph

(defthm alistp-of-topdecl-call-graph
  (b* ((graph (topdecl-call-graph decl)))
    (alistp graph))
  :rule-classes :rewrite)

Theorem: topdecl-call-graph-of-topdecl-fix-decl

(defthm topdecl-call-graph-of-topdecl-fix-decl
  (equal (topdecl-call-graph (topdecl-fix decl))
         (topdecl-call-graph decl)))

Theorem: topdecl-call-graph-topdecl-equiv-congruence-on-decl

(defthm topdecl-call-graph-topdecl-equiv-congruence-on-decl
  (implies (topdecl-equiv decl decl-equiv)
           (equal (topdecl-call-graph decl)
                  (topdecl-call-graph decl-equiv)))
  :rule-classes :congruence)