type_vars_in_term

Term.type_vars_in_term : term -> hol_type list

Return the type variables occurring in a term.

An invocation type_vars_in_term M returns the set of type variables occurring in M.

Failure

Never fails.

Example

> type_vars_in_term (concl boolTheory.ONE_ONE_DEF);
val it = [“:β”, “:α”]: hol_type list

See also

Term.free_vars, Type.type_vars