		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)