		Search-engine friendly clone of the ACL2 documentation.

Rename

Rename-extdecl

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

Definitions and Theorems

Function: rename-extdecl

(defun rename-extdecl (extdecl subst)
 (declare (xargs :guard (and (extdeclp extdecl)
                             (ident-ident-alistp subst))))
 (declare (ignorable extdecl subst))
 (let ((__function__ 'rename-extdecl))
  (declare (ignorable __function__))
  (extdecl-case
       extdecl
       :fundef (extdecl-fundef (rename-fundef extdecl.unwrap subst))
       :decl (extdecl-decl (rename-decl extdecl.unwrap subst))
       :empty (extdecl-empty)
       :asm (extdecl-fix extdecl))))

Theorem: extdeclp-of-rename-extdecl

(defthm extdeclp-of-rename-extdecl
  (b* ((new-extdecl (rename-extdecl extdecl subst)))
    (extdeclp new-extdecl))
  :rule-classes :rewrite)