		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Next-fresh-numbered-name

Specialize next-fresh-numbered-names to a single name.

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

Definitions and Theorems

Function: next-fresh-numbered-name

(defun next-fresh-numbered-name (base index names-to-avoid wrld)
  (declare (xargs :guard (and (symbolp base)
                              (posp index)
                              (symbol-listp names-to-avoid)
                              (plist-worldp wrld))))
  (let ((__function__ 'next-fresh-numbered-name))
    (declare (ignorable __function__))
    (b* (((mv names names-to-avoid)
          (next-fresh-numbered-names (list base)
                                     index names-to-avoid wrld)))
      (mv (car names) names-to-avoid))))