exists_tyvar
Type.exists_tyvar : (hol_type -> bool) -> hol_type -> bool
Checks if a type variable satisfying a given condition exists in a type.
An invocation exists_tyvar P ty searches ty for a type variable
satisfying the predicate P. The value true is returned if the search
is successful; otherwise false is the result.
Failure
If P fails when applied to a type variable encountered in the course
of searching ty.
Example
> exists_tyvar (equal beta) (alpha --> beta --> bool);
val it = true: bool
Comments
This function is more efficient, in some cases, than
exists P o type_vars.