type_var_in : hol_type -> hol_type -> bool
STRUCTURE
Type
SYNOPSIS
Checks if a type variable occurs in a type.
DESCRIPTION
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.
SEEALSO
type_vars, type_varsl, exists_tyvar
HOL  Kananaskis-13