• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
      • Deflist
      • Defalist
      • Memory
      • Defstructure
      • Array1
      • Utilities
        • Defloop
        • Get-option
        • Get-guards-from-body
        • Unique-symbols
        • Pack-intern
        • Pack-string
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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)))