		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Resolve-numbered-name-wildcard

Resolve the wildcard in a numbered name (if any) to the largest index in use for the name's base.

Signature
(resolve-numbered-name-wildcard name wrld) → resolved-name
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: resolved-name — Type (symbolp resolved-name).

If name is a numbered name with base base and the wildcard as index, return the numbered name with base base and index i, where i is the result of max-numbered-name-index-in-use. Otherwise, return name.

Definitions and Theorems

Function: resolve-numbered-name-wildcard

(defun resolve-numbered-name-wildcard (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'resolve-numbered-name-wildcard))
  (declare (ignorable __function__))
  (b* (((mv is-numbered-name base index)
        (check-numbered-name name wrld)))
    (if
      (and is-numbered-name (= index 0))
      (make-numbered-name base
                          (max-numbered-name-index-in-use base wrld)
                          wrld)
      (mbe :logic (symbol-fix name)
           :exec name)))))

Theorem: symbolp-of-resolve-numbered-name-wildcard

(defthm symbolp-of-resolve-numbered-name-wildcard
  (b* ((resolved-name (resolve-numbered-name-wildcard name wrld)))
    (symbolp resolved-name))
  :rule-classes :rewrite)