free_varsl

Term.free_varsl : term list -> term list

Returns the set of free variables in a list of terms.

An invocation free_varsl [t1,...,tn] returns a list representing the set of free term variables occurring in t1,...,tn.

Failure

Never fails.

Example

> free_varsl [Term `x /\ y /\ y ==> x`,
             Term `!x. x ==> p ==> y`];
val it = [“x”, “y”, “p”]: term list

Comments

Code should not depend on how elements are arranged in the result of free_varsl.

free_varsl is not efficient for large terms with many free variables. Demanding applications should be coded with FVL.

See also

Term.FVL, Term.free_vars_lr, Term.free_vars, Term.empty_varset, Type.type_vars