Append as many
(fresh-name-in-world-with-$s name names-to-avoid wrld) → fresh-name
The name returned by this function should be usable for a new function, theorem, constant, etc.
Note that for a constant, the
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
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
If the input name is already new, not among the names to avoid, and not in the main Lisp package, it is returned unchanged.
Function:
(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))