		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Copy-fn-transunit-ensemble

Transform a translation unit ensemble.

Signature
(copy-fn-transunit-ensemble tunits target-fn new-fn) → new-tunits
Arguments: tunits — Guard (transunit-ensemblep tunits).; target-fn — Guard (identp target-fn).; new-fn — Guard (identp new-fn).
Returns: new-tunits — Type (transunit-ensemblep new-tunits).

Definitions and Theorems

Function: copy-fn-transunit-ensemble

(defun copy-fn-transunit-ensemble (tunits target-fn new-fn)
  (declare (xargs :guard (and (transunit-ensemblep tunits)
                              (identp target-fn)
                              (identp new-fn))))
  (declare (xargs :guard (transunit-ensemble-annop tunits)))
  (let ((__function__ 'copy-fn-transunit-ensemble))
    (declare (ignorable __function__))
    (b* (((transunit-ensemble tunits) tunits))
      (transunit-ensemble (copy-fn-filepath-transunit-map
                               tunits.units target-fn new-fn)))))

Theorem: transunit-ensemblep-of-copy-fn-transunit-ensemble

(defthm transunit-ensemblep-of-copy-fn-transunit-ensemble
  (b* ((new-tunits
            (copy-fn-transunit-ensemble tunits target-fn new-fn)))
    (transunit-ensemblep new-tunits))
  :rule-classes :rewrite)