		Search-engine friendly clone of the ACL2 documentation.

Fresh-ident-utility

Fresh-idents

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

Definitions and Theorems

Function: fresh-idents-fn

(defun fresh-idents-fn
       (idents blacklist number-prefix number-suffix)
  (declare (xargs :guard (and (ident-listp idents)
                              (ident-setp blacklist)
                              (stringp number-prefix)
                              (stringp number-suffix))))
  (let ((__function__ 'fresh-idents))
    (declare (ignorable __function__))
    (b* (((when (endp idents)) nil)
         (ident$ (fresh-ident (first idents)
                              blacklist
                              :number-prefix number-prefix
                              :number-suffix number-suffix)))
      (cons ident$
            (fresh-idents (rest idents)
                          (insert ident$ blacklist)
                          :number-prefix number-prefix
                          :number-suffix number-suffix)))))

Theorem: ident-listp-of-fresh-idents

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