Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

type_vars

Type.type_vars : hol_type -> hol_type list

Returns the set of type variables in a type.

An invocation type_vars ty returns a list representing the set of type variables occurring in ty.

Failure

Never fails.

Example

> type_vars ((alpha --> beta) --> bool --> beta);
val it = [“:β”, “:α”]: hol_type list

Comments

Code should not depend on how elements are arranged in the result of type_vars.

See also

Type.type_vars_acc, Type.type_varsl, Type.type_var_in, Type.exists_tyvar, Type.polymorphic, Term.free_vars