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