Compat.tyvars : term -> type list
STRUCTURE
hol88Lib
SYNOPSIS
Returns a list of the type variables free in a term.
DESCRIBE
Found in the hol88 library. When applied to a term, tyvars returns a list (possibly empty) of the type variables which are free in the term.
FAILURE
Never fails. The function is not accessible unless the hol88 library has been loaded.
EXAMPLE
  - theorem "pair" "PAIR";
  |- !x. (FST x,SND x) = x

  - Compat.tyvars (concl PAIR);
  val it = [(==`:'b`==),(==`:'a`==)] : hol_type list

  - Compat.tyvars (--`x + 1 = SUC x`--);
  [] : hol_type list

COMMENTS
tyvars does not appear in hol90; use type_vars_in_term instead. WARNING: the order of the list returned from tyvars need not be the same as that returned from type_vars_in_term.

In the current HOL logic, there is no binding operation for types, so ‘is free in’ is synonymous with ‘appears in’.

SEEALSO
tyvarsl
HOL  Kananaskis-4