Sets the index of a numbered name to the global index for numbered names.
(set-numbered-name-index-to-global name wrld) → new-name
Specialize set-numbered-name-index to use the global index for numbered names.
Function:
(defun set-numbered-name-index-to-global (name wrld) (declare (xargs :guard (and (symbolp name) (plist-worldp wrld)))) (let ((__function__ 'set-numbered-name-index-to-global)) (declare (ignorable __function__)) (set-numbered-name-index name (get-global-numbered-name-index wrld) wrld)))
Theorem:
(defthm symbolp-of-set-numbered-name-index-to-global (b* ((new-name (set-numbered-name-index-to-global name wrld))) (symbolp new-name)) :rule-classes :rewrite)