		Search-engine friendly clone of the ACL2 documentation.

Rename

Code-ensemble-rename

Signature
(code-ensemble-rename code subst) → new-code
Arguments: code — Guard (code-ensemblep code).; subst — Guard (ident-ident-alistp subst).
Returns: new-code — Type (code-ensemblep new-code).

Definitions and Theorems

Function: code-ensemble-rename

(defun code-ensemble-rename (code subst)
  (declare (xargs :guard (and (code-ensemblep code)
                              (ident-ident-alistp subst))))
  (let ((__function__ 'code-ensemble-rename))
    (declare (ignorable __function__))
    (change-code-ensemble
         code
         :transunits
         (transunit-ensemble-rename (code-ensemble->transunits code)
                                    subst))))

Theorem: code-ensemblep-of-code-ensemble-rename

(defthm code-ensemblep-of-code-ensemble-rename
  (b* ((new-code (code-ensemble-rename code subst)))
    (code-ensemblep new-code))
  :rule-classes :rewrite)