		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

Atj-var-add-index

Append a numeric index to a variable.

Signature
(atj-var-add-index var index) → new-var
Arguments: var — Guard (symbolp var).; index — Guard (natp index).
Returns: new-var — Type (symbolp new-var).

This is used to make Java variables unique. The index is appended to the result of atj-var-to-jvar, as explained there.

Definitions and Theorems

Function: atj-var-add-index

(defun atj-var-add-index (var index)
  (declare (xargs :guard (and (symbolp var) (natp index))))
  (let ((__function__ 'atj-var-add-index))
    (declare (ignorable __function__))
    (b* ((index-chars (if (= index 0)
                          nil
                        (append (list #\$)
                                (str::nat-to-dec-chars index))))
         (index-string (implode index-chars)))
      (add-suffix var index-string))))

Theorem: symbolp-of-atj-var-add-index

(defthm symbolp-of-atj-var-add-index
  (b* ((new-var (atj-var-add-index var index)))
    (symbolp new-var))
  :rule-classes :rewrite)