1\DOC FVL
2
3\TYPE {FVL : term list -> term set -> term set}
4
5\SYNOPSIS
6Efficient computation of the set of free variables in a list of terms.
7
8\KEYWORDS
9variable, free, set.
10
11\DESCRIBE
12An invocation {FVL [t1,...,tn] V} adds the set of free variables found
13in {t1,...,tn} to the accumulator {V}.
14
15\FAILURE
16Never fails.
17
18\EXAMPLE
19{
20- FVL [Term `v1 /\ v2 ==> v2 \/ v3`] empty_varset;
21> val it = <set> : term set
22
23- HOLset.listItems it;
24> val it = [`v1`, `v2`, `v3`] : term list
25}
26
27
28\COMMENTS
29Preferable to {free_varsl} when the number of free variables
30becomes large.
31
32\SEEALSO
33HOLset, Term.empty_varset, Term.free_varsl, Term.free_vars.
34\ENDDOC
35