		Search-engine friendly clone of the ACL2 documentation.

Numbered-name-index-start

Get-numbered-name-index-start

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

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

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

Definitions and Theorems

Function: get-numbered-name-index-start

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

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

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