		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))
     (make-transunit
          :decls (copy-fn-extdecl-list tunit.decls target-fn new-fn)
          :info tunit.info))))

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)