polymorphic
Type.polymorphic : hol_type -> bool
Checks if there is a type variable in a type.
An invocation polymorphic ty checks to see if ty has an occurrence
of any type variable. It is equivalent in functionality to
not o null o type_vars, but may be more efficient in some situations,
since it can stop processing once it finds one type variable.
Failure
Never fails.
Example
> polymorphic (bool --> alpha --> ind);
val it = true: bool
Comments
polymorphic is also equivalent to exists_tyvar (K true), and no
faster.