list_mk_fun

boolSyntax.list_mk_fun : hol_type list * hol_type -> hol_type

Iteratively constructs function types.

list_mk_fun([ty1,...,tyn],ty) returns ty1 -> ( ... (tyn -> t)...).

Failure

Never fails.

Example

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

See also

boolSyntax.strip_fun, Type.mk_type, Type.-->