Retrieve the global index for numbered names.
(get-global-numbered-name-index wrld) → global-index
If the global index is not set yet, 1 is returned.
Function:
(defun get-global-numbered-name-index (wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'get-global-numbered-name-index)) (declare (ignorable __function__)) (let ((pair (assoc-eq 'index (table-alist+ 'global-numbered-name-index wrld)))) (cond ((not pair) 1) ((posp (cdr pair)) (cdr pair)) (t (prog2$ (raise "Internal error: ~x0 does not satisfy POSP." (cdr pair)) 1))))))
Theorem:
(defthm posp-of-get-global-numbered-name-index (b* ((global-index (get-global-numbered-name-index wrld))) (posp global-index)) :rule-classes :rewrite)