		Search-engine friendly clone of the ACL2 documentation.

Rename

Rename-extdecl-list

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

Definitions and Theorems

Function: rename-extdecl-list

(defun rename-extdecl-list (extdecls subst)
  (declare (xargs :guard (and (extdecl-listp extdecls)
                              (ident-ident-alistp subst))))
  (declare (ignorable extdecls subst))
  (let ((__function__ 'rename-extdecl-list))
    (declare (ignorable __function__))
    (if (endp extdecls)
        nil
      (cons (rename-extdecl (car extdecls) subst)
            (rename-extdecl-list (cdr extdecls)
                                 subst)))))

Theorem: extdecl-listp-of-rename-extdecl-list

(defthm extdecl-listp-of-rename-extdecl-list
  (b* ((new-extdecls (rename-extdecl-list extdecls subst)))
    (extdecl-listp new-extdecls))
  :rule-classes :rewrite)