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.

See also

Type.type_vars, Type.type_varsl, Type.exists_tyvar