(call-graph-initdeclor-list initdeclors fn-name acc) → call-graph
Function:
(defun call-graph-initdeclor-list (initdeclors fn-name acc) (declare (xargs :guard (and (initdeclor-listp initdeclors) (identp fn-name) (ident-ident-option-set-mapp acc)))) (let ((__function__ 'call-graph-initdeclor-list)) (declare (ignorable __function__)) (if (endp initdeclors) (ident-ident-option-set-map-fix acc) (call-graph-initdeclor-list (rest initdeclors) fn-name (call-graph-initdeclor (first initdeclors) fn-name acc)))))
Theorem:
(defthm ident-ident-option-set-mapp-of-call-graph-initdeclor-list (b* ((call-graph (call-graph-initdeclor-list initdeclors fn-name acc))) (ident-ident-option-set-mapp call-graph)) :rule-classes :rewrite)