Transform a list of external declarations.
(split-fn-extdecl-list target-fn new-fn-name extdecls split-point) → (mv er new-extdecls)
Function:
(defun split-fn-extdecl-list (target-fn new-fn-name extdecls split-point) (declare (xargs :guard (and (identp target-fn) (identp new-fn-name) (extdecl-listp extdecls) (natp split-point)))) (let ((__function__ 'split-fn-extdecl-list)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp extdecls)) (retok nil)) ((erp target-found extdecls1) (split-fn-extdecl target-fn new-fn-name (first extdecls) split-point)) ((when target-found) (retok (append extdecls1 (extdecl-list-fix (rest extdecls))))) ((erp extdecls2) (split-fn-extdecl-list target-fn new-fn-name (rest extdecls) split-point))) (retok (append extdecls1 extdecls2)))))
Theorem:
(defthm extdecl-listp-of-split-fn-extdecl-list.new-extdecls (b* (((mv acl2::?er ?new-extdecls) (split-fn-extdecl-list target-fn new-fn-name extdecls split-point))) (extdecl-listp new-extdecls)) :rule-classes :rewrite)