type_var_in
Type.type_var_in : hol_type -> hol_type -> bool
Checks if a type variable occurs in a type.
An invocation type_var_in tyv ty returns true if tyv occurs in
ty. Otherwise, it returns false.
Failure
Fails if tyv is not a type variable.
Example
> type_var_in alpha (bool --> alpha);
val it = true: bool
> type_var_in alpha bool;
val it = false: bool
Comments
Can be useful in enforcing side conditions on inference rules.