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 = `:'a -> bool -> 'b` : hol_type

See also

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