		Search-engine friendly clone of the ACL2 documentation.

Expressions

Svex-vars

Collect all of the variables from an svex.

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

We collect the set of variables for an svex by computing the exact sets of variables for all of its subexpressions, and unioning them together. This is logically nice to reason about and is sometimes practical to execute.

Although we memoize this function to take advantage of structure sharing, constructing the exact set of variables for every subexpression quickly becomes very memory intensive. For better performance, it is often better to use svex-collect-vars instead.

Subtopics

Svex-alist-vars: Collect all of the variables from all the expressions in an svex-alist.
Svex-collect-vars: Usually faster alternative to svex-vars.
Svexlist-collect-vars: Usually faster alternative to svexlist-vars.
Svexlist-vars: Collect all of the variables from an svexlist.
Svex-vars-basics: Very basic rules about svex-vars