		Search-engine friendly clone of the ACL2 documentation.

Numbered-name-index-end

Get-numbered-name-index-end

Retrieve the current ending marker of the numeric index of numbered names.

Signature
(get-numbered-name-index-end wrld) → end
Arguments: wrld — Guard (plist-worldp wrld).
Returns: end — Type (numbered-name-index-end-p end).

If the ending marker is not set yet, the default is returned.

Definitions and Theorems

Function: get-numbered-name-index-end

(defun get-numbered-name-index-end (wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'get-numbered-name-index-end))
  (declare (ignorable __function__))
  (let ((pair (assoc-eq 'end
                        (table-alist+ 'numbered-name-index-end
                                      wrld))))
   (cond
    ((not pair)
     *default-numbered-name-index-end*)
    ((numbered-name-index-end-p (cdr pair))
     (cdr pair))
    (t
     (prog2$
      (raise
       "Internal error: ~
                             ~x0 does not satisfy NUMBERED-NAME-INDEX-END-P."
       (cdr pair))
      *default-numbered-name-index-end*))))))

Theorem: numbered-name-index-end-p-of-get-numbered-name-index-end

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