		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Copy-fn-filepath-transunit-map

Transform a filepath.

Signature
(copy-fn-filepath-transunit-map map target-fn new-fn) → new-map
Arguments: map — Guard (filepath-transunit-mapp map).; target-fn — Guard (identp target-fn).; new-fn — Guard (identp new-fn).
Returns: new-map — Type (filepath-transunit-mapp new-map), given (filepath-transunit-mapp map).

Definitions and Theorems

Function: copy-fn-filepath-transunit-map

(defun copy-fn-filepath-transunit-map (map target-fn new-fn)
  (declare (xargs :guard (and (filepath-transunit-mapp map)
                              (identp target-fn)
                              (identp new-fn))))
  (declare (xargs :guard (filepath-transunit-map-annop map)))
  (let ((__function__ 'copy-fn-filepath-transunit-map))
    (declare (ignorable __function__))
    (b* (((when (omap::emptyp map)) nil)
         ((mv path tunit) (omap::head map)))
      (omap::update
           (c$::filepath-fix path)
           (copy-fn-transunit tunit target-fn new-fn)
           (copy-fn-filepath-transunit-map (omap::tail map)
                                           target-fn new-fn)))))

Theorem: filepath-transunit-mapp-of-copy-fn-filepath-transunit-map

(defthm filepath-transunit-mapp-of-copy-fn-filepath-transunit-map
 (implies
  (filepath-transunit-mapp map)
  (b*
   ((new-map (copy-fn-filepath-transunit-map map target-fn new-fn)))
   (filepath-transunit-mapp new-map)))
 :rule-classes :rewrite)