		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Transunit-rename

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

Definitions and Theorems

Function: transunit-rename

(defun transunit-rename (transunit subst)
  (declare (xargs :guard (and (transunitp transunit)
                              (ident-ident-alistp subst))))
  (declare (ignorable transunit subst))
  (let ((__function__ 'transunit-rename))
    (declare (ignorable __function__))
    (transunit (extdecl-list-rename (transunit->decls transunit)
                                    subst)
               (c$::transunit->info transunit))))

Theorem: transunitp-of-transunit-rename

(defthm transunitp-of-transunit-rename
  (b* ((fty::result (transunit-rename transunit subst)))
    (transunitp fty::result))
  :rule-classes :rewrite)

Theorem: transunit-rename-of-transunit-fix-transunit

(defthm transunit-rename-of-transunit-fix-transunit
  (equal (transunit-rename (c$::transunit-fix transunit)
                           subst)
         (transunit-rename transunit subst)))

Theorem: transunit-rename-transunit-equiv-congruence-on-transunit

(defthm transunit-rename-transunit-equiv-congruence-on-transunit
  (implies (c$::transunit-equiv transunit transunit-equiv)
           (equal (transunit-rename transunit subst)
                  (transunit-rename transunit-equiv subst)))
  :rule-classes :congruence)

Theorem: transunit-rename-of-ident-ident-alist-fix-subst

(defthm transunit-rename-of-ident-ident-alist-fix-subst
  (equal (transunit-rename transunit (ident-ident-alist-fix subst))
         (transunit-rename transunit subst)))

Theorem: transunit-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm transunit-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (transunit-rename transunit subst)
                  (transunit-rename transunit subst-equiv)))
  :rule-classes :congruence)