		Search-engine friendly clone of the ACL2 documentation.

Rename

Rename-fundef

Signature
(rename-fundef fundef subst) → new-fundef
Arguments: fundef — Guard (fundefp fundef).; subst — Guard (ident-ident-alistp subst).
Returns: new-fundef — Type (fundefp new-fundef).

Definitions and Theorems

Function: rename-fundef

(defun rename-fundef (fundef subst)
  (declare (xargs :guard (and (fundefp fundef)
                              (ident-ident-alistp subst))))
  (declare (ignorable fundef subst))
  (let ((__function__ 'rename-fundef))
    (declare (ignorable __function__))
    (b* (((fundef fundef) fundef))
      (make-fundef :extension fundef.extension
                   :spec (rename-decl-spec-list fundef.spec subst)
                   :declor (rename-declor fundef.declor subst)
                   :asm? fundef.asm?
                   :attribs fundef.attribs
                   :decls (rename-decl-list fundef.decls subst)
                   :body (rename-stmt fundef.body subst)))))

Theorem: fundefp-of-rename-fundef

(defthm fundefp-of-rename-fundef
  (b* ((new-fundef (rename-fundef fundef subst)))
    (fundefp new-fundef))
  :rule-classes :rewrite)