		Search-engine friendly clone of the ACL2 documentation.

Rename

Rename-filepath-transunit-map

Signature
(rename-filepath-transunit-map map subst) → new-map
Arguments: map — Guard (filepath-transunit-mapp map).; subst — Guard (ident-ident-alistp subst).
Returns: new-map — Type (filepath-transunit-mapp new-map), given (filepath-transunit-mapp map).

Definitions and Theorems

Function: rename-filepath-transunit-map

(defun rename-filepath-transunit-map (map subst)
  (declare (xargs :guard (and (filepath-transunit-mapp map)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'rename-filepath-transunit-map))
    (declare (ignorable __function__))
    (b* (((when (omap::emptyp map)) nil)
         ((mv path tunit) (omap::head map))
         (new-path (deftrans-filepath path "RENAME"))
         (new-tunit (rename-transunit tunit subst))
         (new-map (rename-filepath-transunit-map (omap::tail map)
                                                 subst)))
      (omap::update new-path new-tunit new-map))))

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

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