		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Next-numbered-name

Next numbered name with the same base.

Signature
(next-numbered-name name wrld) → new-name
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: new-name — A symbol.

If name is a numbered name with base base and index i, return the numbered name with base base and index j, where j is the smallest integer larger than i such that the numbered name with base base and index j is not in the ACL2 world. If name is a numbered name with base base and the wildcard as index, the behavior is the same as if this function were called on the result of resolve-numbered-name-wildcard on name. If name is not a numbered name, treat it as if it had numeric index 0, i.e. return the numbered name with base name and index j, where j is the smallest positive integer such that the numbered name with base name and index j is not in the ACL2 world.

This function is independent from the global index for numbered names.

Definitions and Theorems

Function: next-numbered-name-aux

(defun next-numbered-name-aux (base current-index wrld)
  (declare (xargs :guard (and (symbolp base)
                              (posp current-index)
                              (plist-worldp wrld))))
  (let ((__function__ 'next-numbered-name-aux))
    (declare (ignorable __function__))
    (let ((name (make-numbered-name base current-index wrld)))
      (if (logical-namep name wrld)
          (next-numbered-name-aux base (1+ current-index)
                                  wrld)
        current-index))))

Function: next-numbered-name

(defun next-numbered-name (name wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (let ((__function__ 'next-numbered-name))
  (declare (ignorable __function__))
  (b* (((mv is-numbered-name base index)
        (check-numbered-name name wrld)))
    (if is-numbered-name
     (let
      ((next-index
            (if (= index 0)
                (next-numbered-name-aux
                     base
                     (1+ (max-numbered-name-index-in-use base wrld))
                     wrld)
              (next-numbered-name-aux base (1+ index)
                                      wrld))))
      (make-numbered-name base next-index wrld))
     (let ((next-index (next-numbered-name-aux name 1 wrld)))
       (make-numbered-name name next-index wrld))))))