		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-init-declor-list

Signature
(call-graph-init-declor-list initdeclors fn-name filepath valid-table call-graph) → call-graph$
Arguments: initdeclors — Guard (init-declor-listp initdeclors).; fn-name — Guard (qualified-identp fn-name).; 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-init-declor-list

(defun call-graph-init-declor-list
       (initdeclors fn-name filepath valid-table call-graph)
 (declare (xargs :guard (and (init-declor-listp initdeclors)
                             (qualified-identp fn-name)
                             (filepathp filepath)
                             (valid-tablep valid-table)
                             (call-graphp call-graph))))
 (let ((__function__ 'call-graph-init-declor-list))
  (declare (ignorable __function__))
  (if (endp initdeclors)
      (call-graph-fix call-graph)
   (call-graph-init-declor-list
        (rest initdeclors)
        fn-name filepath valid-table
        (call-graph-init-declor (first initdeclors)
                                fn-name
                                filepath valid-table call-graph)))))

Theorem: call-graphp-of-call-graph-init-declor-list

(defthm call-graphp-of-call-graph-init-declor-list
 (b*
  ((call-graph$
     (call-graph-init-declor-list initdeclors fn-name
                                  filepath valid-table call-graph)))
  (call-graphp call-graph$))
 :rule-classes :rewrite)