		Search-engine friendly clone of the ACL2 documentation.

Call-graph

Call-graph-extdecl

Signature
(call-graph-extdecl extdecl acc) → call-graph
Arguments: extdecl — Guard (extdeclp extdecl).; 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-extdecl

(defun call-graph-extdecl (extdecl acc)
  (declare (xargs :guard (and (extdeclp extdecl)
                              (ident-ident-option-set-mapp acc))))
  (let ((__function__ 'call-graph-extdecl))
    (declare (ignorable __function__))
    (extdecl-case extdecl
                  :fundef (call-graph-fundef extdecl.unwrap acc)
                  :decl (ident-ident-option-set-map-fix acc)
                  :empty (ident-ident-option-set-map-fix acc)
                  :asm (ident-ident-option-set-map-fix acc))))

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

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