		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Rename-fn-fundef

Signature
(rename-fn-fundef fundef old-fn new-fn) → new-fundef
Arguments: fundef — Guard (fundefp fundef).; old-fn — Guard (identp old-fn).; new-fn — Guard (identp new-fn).
Returns: new-fundef — Type (fundefp new-fundef).

Definitions and Theorems

Function: rename-fn-fundef

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

Theorem: fundefp-of-rename-fn-fundef

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