		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-ext-declon

Signature
(call-graph-ext-declon extdecl filepath valid-table call-graph) → call-graph$
Arguments: extdecl — Guard (ext-declonp extdecl).; filepath — Guard (filepathp filepath).; valid-table — Guard (valid-tablep valid-table).; call-graph — Guard (call-graphp call-graph).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-ext-declon

(defun call-graph-ext-declon
       (extdecl filepath valid-table call-graph)
  (declare (xargs :guard (and (ext-declonp extdecl)
                              (filepathp filepath)
                              (valid-tablep valid-table)
                              (call-graphp call-graph))))
  (let ((__function__ 'call-graph-ext-declon))
    (declare (ignorable __function__))
    (ext-declon-case
         extdecl
         :fundef (call-graph-fundef extdecl.fundef
                                    filepath valid-table call-graph)
         :declon (call-graph-fix call-graph)
         :empty (call-graph-fix call-graph)
         :asm (call-graph-fix call-graph))))

Theorem: call-graphp-of-call-graph-ext-declon

(defthm call-graphp-of-call-graph-ext-declon
 (b* ((call-graph$
           (call-graph-ext-declon extdecl
                                  filepath valid-table call-graph)))
   (call-graphp call-graph$))
 :rule-classes :rewrite)