		Search-engine friendly clone of the ACL2 documentation.

Utilities

Unique-symbols

Return a list of symbols guaranteed unique with respect to a symbolic seed and every symbol in a list of symbols.

Given a symbolic seed, we generate symbols <seed>0, <seed>1, etc. until we have generated n symbols not appearing in sym-list. This is a 'poor-man's' GENSYM, and is the best we can do without STATE. All generated symbols are INTERNed in the package of seed.

Definitions and Theorems

Function: unique-symbols

(defun unique-symbols (n seed sym-list)
  (declare (xargs :guard (and (naturalp n)
                              (symbolp seed)
                              (symbol-listp sym-list))))
  (reverse (unique-symbols1 n seed sym-list 0 nil)))