(rename-label label subst) → new-label
Function:
(defun rename-label (label subst) (declare (xargs :guard (and (labelp label) (ident-ident-alistp subst)))) (declare (ignorable label subst)) (let ((__function__ 'rename-label)) (declare (ignorable __function__)) (label-case label :name (label-fix label) :const (label-const (rename-const-expr label.unwrap subst)) :default (label-fix label))))
Theorem:
(defthm labelp-of-rename-label (b* ((new-label (rename-label label subst))) (labelp new-label)) :rule-classes :rewrite)