		Search-engine friendly clone of the ACL2 documentation.

Indexed-names

Iname

Create an indexed name, from a base and an index.

Signature
(iname base i) → name
Arguments: base — Guard (stringp base).; i — Guard (natp i).
Returns: name — Type (stringp name).

Definitions and Theorems

Function: iname

(defun iname (base i)
  (declare (xargs :guard (and (stringp base) (natp i))))
  (let ((__function__ 'iname))
    (declare (ignorable __function__))
    (str::cat base "_" (str::nat-to-dec-string i))))

Theorem: stringp-of-iname

(defthm stringp-of-iname
  (b* ((name (iname base i)))
    (stringp name))
  :rule-classes :rewrite)

Theorem: iname-of-nfix-i

(defthm iname-of-nfix-i
  (equal (iname base (nfix i))
         (iname base i)))

Theorem: iname-nat-equiv-congruence-on-i

(defthm iname-nat-equiv-congruence-on-i
  (implies (acl2::nat-equiv i i-equiv)
           (equal (iname base i)
                  (iname base i-equiv)))
  :rule-classes :congruence)

Theorem: iname-not-equal-to-base

(defthm iname-not-equal-to-base
  (implies (stringp base)
           (not (equal (iname base i) base))))

Subtopics

Iname-injective-on-index: The function iname is injective over the index.