		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-suffix-signals

Convert a list of atoms into a list of symbols with some suffix.

Signature
(stv-suffix-signals x suffix) → symbols
Arguments: x — Guard (atom-listp x).; suffix — Guard (stringp suffix).
Returns: symbols — Type (symbol-listp symbols).

Definitions and Theorems

Function: stv-suffix-signals

(defun stv-suffix-signals (x suffix)
  (declare (xargs :guard (and (atom-listp x) (stringp suffix))))
  (let ((__function__ 'stv-suffix-signals))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (intern$ (str::cat (stringify (car x)) suffix)
                     "ACL2")
            (stv-suffix-signals (cdr x) suffix)))))

Theorem: symbol-listp-of-stv-suffix-signals

(defthm symbol-listp-of-stv-suffix-signals
  (b* ((symbols (stv-suffix-signals x suffix)))
    (symbol-listp symbols))
  :rule-classes :rewrite)