		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Call-graph-decl

Signature
(call-graph-decl decl fn-name acc) → call-graph
Arguments: decl — Guard (declp decl).; fn-name — Guard (identp fn-name).; acc — Guard (ident-ident-option-set-mapp acc).
Returns: call-graph — Type (ident-ident-option-set-mapp call-graph).

Definitions and Theorems

Function: call-graph-decl

(defun call-graph-decl (decl fn-name acc)
 (declare (xargs :guard (and (declp decl)
                             (identp fn-name)
                             (ident-ident-option-set-mapp acc))))
 (let ((__function__ 'call-graph-decl))
  (declare (ignorable __function__))
  (decl-case
      decl
      :decl (call-graph-initdeclor-list decl.init fn-name acc)
      :statassert (call-graph-statassert decl.unwrap fn-name acc))))

Theorem: ident-ident-option-set-mapp-of-call-graph-decl

(defthm ident-ident-option-set-mapp-of-call-graph-decl
  (b* ((call-graph (call-graph-decl decl fn-name acc)))
    (ident-ident-option-set-mapp call-graph))
  :rule-classes :rewrite)