type_vars_in_term : term -> hol_type list
- SYNOPSIS
-
Returns the set of type variables used in a term.
- DESCRIPTION
-
The call type_vars_in_term t returns the set of all type variables occurring
anywhere inside any subterm of t.
- FAILURE CONDITIONS
-
Never fails.
- EXAMPLE
-
Note that the list of types occurring somewhere in the term may be larger than
the set of type variables in the term's toplevel type. For example:
# type_vars_in_term `!x:A. x = x`;;
val it : hol_type list = [`:A`]
# tyvars(type_of `!x:A. x = x`);;
val it : hol_type list = []
- SEE ALSO
-
frees, tyvars.