		Search-engine friendly clone of the ACL2 documentation.

Stv-gensyms

Stv-gensyms-aux

Signature
(stv-gensyms-aux prefix n acc) → syms
Arguments: prefix — Guard (stringp prefix).; n — Guard (natp n).
Returns: syms — Type (symbol-listp syms), given (symbol-listp acc).

Definitions and Theorems

Function: stv-gensyms-aux

(defun stv-gensyms-aux (prefix n acc)
  (declare (xargs :guard (and (stringp prefix) (natp n))))
  (let ((__function__ 'stv-gensyms-aux))
    (declare (ignorable __function__))
    (b* (((when (zp n)) acc)
         (n (- n 1))
         (sym1 (intern$ (str::cat prefix "[" (str::natstr n)
                                  "]")
                        "ACL2")))
      (stv-gensyms-aux prefix n (cons sym1 acc)))))

Theorem: symbol-listp-of-stv-gensyms-aux

(defthm symbol-listp-of-stv-gensyms-aux
  (implies (symbol-listp acc)
           (b* ((syms (stv-gensyms-aux prefix n acc)))
             (symbol-listp syms)))
  :rule-classes :rewrite)

Theorem: len-of-stv-gensyms-aux

(defthm len-of-stv-gensyms-aux
  (equal (len (stv-gensyms-aux prefix n acc))
         (+ (len acc) (nfix n))))