		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Copy-fn-transunit

Transform a translation unit.

Signature
(copy-fn-transunit tunit target-fn new-fn) → new-tunit
Arguments: tunit — Guard (transunitp tunit).; target-fn — Guard (identp target-fn).; new-fn — Guard (identp new-fn).
Returns: new-tunit — Type (transunitp new-tunit).

Definitions and Theorems

Function: copy-fn-transunit

(defun copy-fn-transunit (tunit target-fn new-fn)
  (declare (xargs :guard (and (transunitp tunit)
                              (identp target-fn)
                              (identp new-fn))))
  (let ((__function__ 'copy-fn-transunit))
    (declare (ignorable __function__))
    (b* (((transunit tunit) tunit))
      (transunit
           (copy-fn-extdecl-list tunit.decls target-fn new-fn)))))

Theorem: transunitp-of-copy-fn-transunit

(defthm transunitp-of-copy-fn-transunit
  (b* ((new-tunit (copy-fn-transunit tunit target-fn new-fn)))
    (transunitp new-tunit))
  :rule-classes :rewrite)