		Search-engine friendly clone of the ACL2 documentation.

Rename

Rename-transunit

Signature
(rename-transunit tunit subst) → new-tunit
Arguments: tunit — Guard (transunitp tunit).; subst — Guard (ident-ident-alistp subst).
Returns: new-tunit — Type (transunitp new-tunit).

Definitions and Theorems

Function: rename-transunit

(defun rename-transunit (tunit subst)
  (declare (xargs :guard (and (transunitp tunit)
                              (ident-ident-alistp subst))))
  (declare (ignorable tunit subst))
  (let ((__function__ 'rename-transunit))
    (declare (ignorable __function__))
    (b* (((transunit tunit) tunit))
      (transunit (rename-extdecl-list tunit.decls subst)))))

Theorem: transunitp-of-rename-transunit

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