		Search-engine friendly clone of the ACL2 documentation.

Fresh-ident-utility

Fresh-ident

Signature
(fresh-ident ident blacklist &key (number-prefix '"_") (number-suffix '"")) → ident$
Arguments: ident — Guard (identp ident).; blacklist — Guard (ident-setp blacklist).; number-prefix — Guard (stringp number-prefix).; number-suffix — Guard (stringp number-suffix).
Returns: ident$ — Type (identp ident$).

Definitions and Theorems

Function: fresh-ident-fn

(defun fresh-ident-fn (ident blacklist number-prefix number-suffix)
  (declare (xargs :guard (and (identp ident)
                              (ident-setp blacklist)
                              (stringp number-prefix)
                              (stringp number-suffix))))
  (let ((__function__ 'fresh-ident))
    (declare (ignorable __function__))
    (b* ((ident-string (ident->unwrap ident))
         ((unless (stringp ident-string))
          (raise "Identifier ~x0 does not contain a string."
                 ident)
          (c$::irr-ident))
         (string-blacklist (map-ident->unwrap blacklist)))
      (ident (fresh-string-wrt ident-string number-prefix
                               number-suffix string-blacklist)))))

Theorem: identp-of-fresh-ident

(defthm identp-of-fresh-ident
  (b*
   ((ident$ (fresh-ident-fn ident
                            blacklist number-prefix number-suffix)))
   (identp ident$))
  :rule-classes :rewrite)