(rename-decl decl subst) → new-decl
Function:
(defun rename-decl (decl subst) (declare (xargs :guard (and (declp decl) (ident-ident-alistp subst)))) (declare (ignorable decl subst)) (let ((__function__ 'rename-decl)) (declare (ignorable __function__)) (decl-case decl :decl (make-decl-decl :extension decl.extension :specs (rename-declspec-list decl.specs subst) :init (rename-initdeclor-list decl.init subst) :asm? decl.asm? :attrib decl.attrib) :statassert (decl-statassert (rename-statassert decl.unwrap subst)))))
Theorem:
(defthm declp-of-rename-decl (b* ((new-decl (rename-decl decl subst))) (declp new-decl)) :rule-classes :rewrite)