Transform a filepath.
(split-fn-filepath-transunit-map target-fn new-fn-name map split-point) → (mv er new-map)
Function:
(defun split-fn-filepath-transunit-map (target-fn new-fn-name map split-point) (declare (xargs :guard (and (identp target-fn) (identp new-fn-name) (filepath-transunit-mapp map) (natp split-point)))) (let ((__function__ 'split-fn-filepath-transunit-map)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (omap::emptyp map)) (retok nil)) ((mv path tunit) (omap::head map)) (new-path (deftrans-filepath path "SPLIT-FN")) ((erp new-tunit) (split-fn-transunit target-fn new-fn-name tunit split-point)) ((erp new-map) (split-fn-filepath-transunit-map target-fn new-fn-name (omap::tail map) split-point))) (retok (omap::update new-path new-tunit new-map)))))
Theorem:
(defthm filepath-transunit-mapp-of-split-fn-filepath-transunit-map.new-map (implies (filepath-transunit-mapp map) (b* (((mv acl2::?er ?new-map) (split-fn-filepath-transunit-map target-fn new-fn-name map split-point))) (filepath-transunit-mapp new-map))) :rule-classes :rewrite)