		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-gensyms

Generate a list of symbols, (foo[0] ... foo[n-1]).

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

Definitions and Theorems

Function: stv-gensyms

(defun stv-gensyms (prefix n)
  (declare (xargs :guard (and (stringp prefix) (natp n))))
  (let ((__function__ 'stv-gensyms))
    (declare (ignorable __function__))
    (stv-gensyms-aux prefix n nil)))

Theorem: symbol-listp-of-stv-gensyms

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

Theorem: len-of-stv-gensyms

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

Subtopics

Stv-gensyms-aux