		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Next-fresh-numbered-names

Add to each of the given bases the lowest index, starting with the given index, such that the resulting names are not already in use.

Signature
(next-fresh-numbered-names bases index names-to-avoid wrld) → (mv names new-names-to-avoid)
Arguments: bases — Guard (symbol-listp bases).; index — Guard (posp index).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: names — A symbol-listp.; new-names-to-avoid — A symbol-listp.

Definitions and Theorems

Function: next-fresh-numbered-names

(defun next-fresh-numbered-names (bases index names-to-avoid wrld)
 (declare (xargs :guard (and (symbol-listp bases)
                             (posp index)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'next-fresh-numbered-names))
  (declare (ignorable __function__))
  (b*
   ((names (make-numbered-name-list bases (repeat (len bases) index)
                                    wrld))
    ((when (and (null (fresh-name-listp-msg-weak names 'function
                                                 wrld))
                (not (intersectp-eq names names-to-avoid))))
     (mv names (append names names-to-avoid))))
   (next-fresh-numbered-names bases (1+ index)
                              names-to-avoid wrld))))