		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-filepath-transunit-map

Signature
(const-prop-filepath-transunit-map map) → new-map
Arguments: map — Guard (filepath-transunit-mapp map).
Returns: new-map — Type (filepath-transunit-mapp new-map), given (filepath-transunit-mapp map).

Definitions and Theorems

Function: const-prop-filepath-transunit-map

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

Theorem: filepath-transunit-mapp-of-const-prop-filepath-transunit-map

(defthm filepath-transunit-mapp-of-const-prop-filepath-transunit-map
  (implies (filepath-transunit-mapp map)
           (b* ((new-map (const-prop-filepath-transunit-map map)))
             (filepath-transunit-mapp new-map)))
  :rule-classes :rewrite)