		Search-engine friendly clone of the ACL2 documentation.

Fresh-ident-utility

Fresh-string-wrt

Signature
(fresh-string-wrt base number-prefix number-suffix blacklist) → string
Arguments: base — Guard (stringp base).; number-prefix — Guard (stringp number-prefix).; number-suffix — Guard (stringp number-suffix).; blacklist — Guard (acl2::string-setp blacklist).
Returns: string — Type (stringp string).

Definitions and Theorems

Function: fresh-string-wrt

(defun fresh-string-wrt (base number-prefix number-suffix blacklist)
  (declare (xargs :guard (and (stringp base)
                              (stringp number-prefix)
                              (stringp number-suffix)
                              (acl2::string-setp blacklist))))
  (let ((__function__ 'fresh-string-wrt))
    (declare (ignorable __function__))
    (if (in base blacklist)
        (fresh-numbered-string-wrt
             base
             number-prefix 0 number-suffix blacklist)
      (mbe :logic (if (stringp base) base "")
           :exec base))))

Theorem: stringp-of-fresh-string-wrt

(defthm stringp-of-fresh-string-wrt
  (b*
    ((string
          (fresh-string-wrt base
                            number-prefix number-suffix blacklist)))
    (stringp string))
  :rule-classes :rewrite)