frees : term -> term list
- SYNOPSIS
-
Returns a list of the variables free in a term.
- DESCRIPTION
-
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
-
Never fails.
- EXAMPLE
-
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
-
atoms, freesl, free_in, thm_frees, variables.