		Search-engine friendly clone of the ACL2 documentation.

Specialize

Specialize-filepath-transunit-map

Transform a filepath.

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

Definitions and Theorems

Function: specialize-filepath-transunit-map

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

Theorem: filepath-transunit-mapp-of-specialize-filepath-transunit-map

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