frees : term -> term list
Returns a list of the variables free in a term.
When applied to a term, frees returns a list of the free variables in
that term. There are no repetitions in the list produced even if there are
multiple free instances of some variables.
- FAILURE CONDITIONS
Clearly in the following term, x and y are free, whereas z is bound:
# frees `x = 1 /\ y = 2 /\ !z. z >= 0`;;
val it : term list = [`x`; `y`]
- SEE ALSO
freesl, free_in, thm_frees, variables.