		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Make-numbered-name

Construct a numbered name from a base and an index (or wildcard).

Signature
(make-numbered-name base index-or-wildcard wrld) → name
Arguments: base — Guard (symbolp base).; index-or-wildcard — Positive index, or 0 for the wildcard.
Guard (natp index-or-wildcard).; wrld — Guard (plist-worldp wrld).
Returns: name — Type (symbolp name).

Definitions and Theorems

Function: make-numbered-name

(defun make-numbered-name (base index-or-wildcard wrld)
 (declare (xargs :guard (and (symbolp base)
                             (natp index-or-wildcard)
                             (plist-worldp wrld))))
 (let ((__function__ 'make-numbered-name))
   (declare (ignorable __function__))
   (b*
     ((base-chars (explode (symbol-name base)))
      (index-start-chars
           (explode (get-numbered-name-index-start wrld)))
      (index-end-chars (explode (get-numbered-name-index-end wrld)))
      (index-or-wildcard-chars
           (if (zp index-or-wildcard)
               (explode (get-numbered-name-index-wildcard wrld))
             (str::nat-to-dec-chars index-or-wildcard)))
      (name-chars (append base-chars index-start-chars
                          index-or-wildcard-chars
                          index-end-chars)))
     (if (equal (symbol-package-name base)
                *main-lisp-package-name*)
         (intern (implode name-chars) "ACL2")
       (intern-in-package-of-symbol (implode name-chars)
                                    base)))))

Theorem: symbolp-of-make-numbered-name

(defthm symbolp-of-make-numbered-name
  (b* ((name (make-numbered-name base index-or-wildcard wrld)))
    (symbolp name))
  :rule-classes :rewrite)