free_vars_lr : term -> term list

- STRUCTURE
- SYNOPSIS
- Returns the set of free variables in a term, in order.
- DESCRIPTION
- An invocation free_vars_lr ty returns a list representing the set of type variables occurring in ty. The list will be in order of variable occurrence when scanning the parse tree of the term from left to right. This is usually, but need not be, the textual order when the term is printed.
- FAILURE
- Never fails.
- EXAMPLE
- free_vars_lr (Term `x /\ y /\ y ==> z`); > val it = [`x`, `y`, `z`] : term list

- COMMENTS
- free_vars_lr is not efficient for large terms with many free variables. More strenuous applications should use high performance set implementations available in the Standard ML Basis Library.
- USES
- free_vars_lr can be used to build pleasing quantifier prefixes.
- SEEALSO

HOL Kananaskis-14