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.