		Search-engine friendly clone of the ACL2 documentation.

Numbered-names

Set-numbered-name-index

Sets the index of a numbered name.

Signature
(set-numbered-name-index name index wrld) → new-name
Arguments: name — Guard (symbolp name).; index — Guard (posp index).; wrld — Guard (plist-worldp wrld).
Returns: new-name — Type (symbolp new-name).

If name is a numbered name with base base, return the numbered name with base base and index index (i.e. replace the index). Otherwise, return the numbered name with base name and index index (i.e. add the index).

Definitions and Theorems

Function: set-numbered-name-index

(defun set-numbered-name-index (name index wrld)
  (declare (xargs :guard (and (symbolp name)
                              (posp index)
                              (plist-worldp wrld))))
  (let ((__function__ 'set-numbered-name-index))
    (declare (ignorable __function__))
    (b* (((mv is-numbered-name base &)
          (check-numbered-name name wrld)))
      (if is-numbered-name (make-numbered-name base index wrld)
        (make-numbered-name name index wrld)))))

Theorem: symbolp-of-set-numbered-name-index

(defthm symbolp-of-set-numbered-name-index
  (b* ((new-name (set-numbered-name-index name index wrld)))
    (symbolp new-name))
  :rule-classes :rewrite)