		Search-engine friendly clone of the ACL2 documentation.

System-utilities-non-built-in

Fresh-name-in-world-with-$s

Append as many $ signs to a name as needed to make the name new in the world, i.e. not already in use, and not among a given list of names to avoid.

Signature
(fresh-name-in-world-with-$s name names-to-avoid wrld) → fresh-name
Arguments: name — Guard (and (symbolp name) (not (keywordp name))).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: fresh-name — A symbolp.

The name returned by this function should be usable for a new function, theorem, constant, etc.

Note that for a constant, the $ signs are appended before the final * character.

The input name must not be a keyword, because it would remain a keyword (which cannot be the name of a function, theorem, etc.) when $ signs are appended to it.

Since symbols in the main Lisp package are not usable to name new functions, theorems, etc., if the input name is in the main Lisp package, the output name is in the "ACL2" package, and has at least one $ appended to it.

If the input name is already new, not among the names to avoid, and not in the main Lisp package, it is returned unchanged.

Definitions and Theorems

Function: fresh-name-in-world-with-$s

(defun
 fresh-name-in-world-with-$s
 (name names-to-avoid wrld)
 (declare (xargs :guard (and (and (symbolp name)
                                  (not (keywordp name)))
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (if
   (or (logical-namep name wrld)
       (member name names-to-avoid)
       (equal (symbol-package-name name)
              *main-lisp-package-name*))
   (fresh-name-in-world-with-$s (add-suffix-to-fn-or-const name "$")
                                names-to-avoid wrld)
   name))