		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Call-graph-filepath-transunit-map

Signature
(call-graph-filepath-transunit-map map call-graph) → call-graph$
Arguments: map — Guard (filepath-transunit-mapp map).; call-graph — Guard (call-graphp call-graph).
Returns: call-graph$ — Type (call-graphp call-graph$).

Definitions and Theorems

Function: call-graph-filepath-transunit-map

(defun call-graph-filepath-transunit-map (map call-graph)
  (declare (xargs :guard (and (filepath-transunit-mapp map)
                              (call-graphp call-graph))))
  (declare (xargs :guard (filepath-transunit-map-annop map)))
  (let ((__function__ 'call-graph-filepath-transunit-map))
    (declare (ignorable __function__))
    (if (omap::emptyp map)
        (call-graph-fix call-graph)
      (call-graph-filepath-transunit-map
           (omap::tail map)
           (call-graph-transunit (omap::head-key map)
                                 (omap::head-val map)
                                 call-graph)))))

Theorem: call-graphp-of-call-graph-filepath-transunit-map

(defthm call-graphp-of-call-graph-filepath-transunit-map
 (b*
  ((call-graph$ (call-graph-filepath-transunit-map map call-graph)))
  (call-graphp call-graph$))
 :rule-classes :rewrite)