		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv->vars

Get a list of an STV's simulation variables (both inputs and outputs).

Signature
(stv->vars x) → vars
Arguments: x — Guard (processed-stv-p x).
Returns: vars — Should be a symbol-listp in practice.

Definitions and Theorems

Function: stv->vars

(defun stv->vars (x)
  (declare (xargs :guard (processed-stv-p x)))
  (let ((__function__ 'stv->vars))
    (declare (ignorable __function__))
    (append (stv->ins x) (stv->outs x))))