		Search-engine friendly clone of the ACL2 documentation.

Numbered-name-index-wildcard

Get-numbered-name-index-wildcard

Retrieve the current wildcard for the numeric index of numbered names.

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

If the wildcard is not set yet, the default is returned.

Definitions and Theorems

Function: get-numbered-name-index-wildcard

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

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

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