		Search-engine friendly clone of the ACL2 documentation.

Global-numbered-name-index

Get-global-numbered-name-index

Retrieve the global index for numbered names.

Signature
(get-global-numbered-name-index wrld) → global-index
Arguments: wrld — Guard (plist-worldp wrld).
Returns: global-index — A posp.
Type (posp global-index).

If the global index is not set yet, 1 is returned.

Definitions and Theorems

Function: get-global-numbered-name-index

(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: posp-of-get-global-numbered-name-index

(defthm posp-of-get-global-numbered-name-index
  (b* ((global-index (get-global-numbered-name-index wrld)))
    (posp global-index))
  :rule-classes :rewrite)