(rename-decl-list decls subst) → new-decls
Function:
(defun rename-decl-list (decls subst) (declare (xargs :guard (and (decl-listp decls) (ident-ident-alistp subst)))) (declare (ignorable decls subst)) (let ((__function__ 'rename-decl-list)) (declare (ignorable __function__)) (if (endp decls) nil (cons (rename-decl (car decls) subst) (rename-decl-list (cdr decls) subst)))))
Theorem:
(defthm decl-listp-of-rename-decl-list (b* ((new-decls (rename-decl-list decls subst))) (decl-listp new-decls)) :rule-classes :rewrite)