		Search-engine friendly clone of the ACL2 documentation.

Fresh-ident-utility

Make-numbered-string

Signature
(make-numbered-string base number-prefix number number-suffix) → string
Arguments: base — Guard (stringp base).; number-prefix — Guard (stringp number-prefix).; number — Guard (natp number).; number-suffix — Guard (stringp number-suffix).
Returns: string — Type (stringp string).

Definitions and Theorems

Function: make-numbered-string

(defun make-numbered-string
       (base number-prefix number number-suffix)
  (declare (xargs :guard (and (stringp base)
                              (stringp number-prefix)
                              (natp number)
                              (stringp number-suffix))))
  (let ((__function__ 'make-numbered-string))
    (declare (ignorable __function__))
    (concatenate
         'string
         base number-prefix
         (acl2::implode (explode-nonnegative-integer number 10 nil))
         number-suffix)))

Theorem: stringp-of-make-numbered-string

(defthm stringp-of-make-numbered-string
  (b*
   ((string
         (make-numbered-string base
                               number-prefix number number-suffix)))
   (stringp string))
  :rule-classes :rewrite)