		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Rename-fn-transunit

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

Definitions and Theorems

Function: rename-fn-transunit

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

Theorem: transunitp-of-rename-fn-transunit

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