		Search-engine friendly clone of the ACL2 documentation.

Svexlist-vars

Collect all of the variables from an svexlist.

Signature
(svexlist-vars x) → vars
Arguments: x — Expression list to collect variables from.
Guard (svexlist-p x).
Returns: vars — An ordered set of all variables used in any expression in x.
Type (and (svarlist-p vars) (setp vars)).

See svex-vars. This just unions together the svex-vars of all of the expressions in x.

Like svex-vars, this is logically nice but can be very memory intensive. It is often better to use svexlist-collect-vars instead.