(rename-initdeclor initdeclor subst) → new-initdeclor
Function:
(defun rename-initdeclor (initdeclor subst) (declare (xargs :guard (and (initdeclorp initdeclor) (ident-ident-alistp subst)))) (declare (ignorable initdeclor subst)) (let ((__function__ 'rename-initdeclor)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor)) (make-initdeclor :declor (rename-declor initdeclor.declor subst) :init? (rename-initer-option initdeclor.init? subst)))))
Theorem:
(defthm initdeclorp-of-rename-initdeclor (b* ((new-initdeclor (rename-initdeclor initdeclor subst))) (initdeclorp new-initdeclor)) :rule-classes :rewrite)