Sets the index of a numbered name.
(set-numbered-name-index name index wrld) → new-name
If
Function:
(defun set-numbered-name-index (name index wrld) (declare (xargs :guard (and (symbolp name) (posp index) (plist-worldp wrld)))) (let ((__function__ 'set-numbered-name-index)) (declare (ignorable __function__)) (b* (((mv is-numbered-name base &) (check-numbered-name name wrld))) (if is-numbered-name (make-numbered-name base index wrld) (make-numbered-name name index wrld)))))
Theorem:
(defthm symbolp-of-set-numbered-name-index (b* ((new-name (set-numbered-name-index name index wrld))) (symbolp new-name)) :rule-classes :rewrite)