		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-filepath-transunit-map

Transform a map from file paths to translation units.

Signature
(simpadd0-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).

We transform both the file paths and the translation units.

Definitions and Theorems

Function: simpadd0-filepath-transunit-map

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

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

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

Theorem: filepath-transunit-map-unambp-of-simpadd-filepath-transunit-map

(defthm
    filepath-transunit-map-unambp-of-simpadd-filepath-transunit-map
  (implies (filepath-transunit-mapp map)
           (b* ((?new-map (simpadd0-filepath-transunit-map map)))
             (filepath-transunit-map-unambp new-map))))