----------------------------------------------------------------------
strip_fun                                                 (boolSyntax)
----------------------------------------------------------------------
strip_fun : hol_type -> hol_type list * hol_type

SYNOPSIS
Iteratively breaks apart function types.

DESCRIBE
If {fty} is of the form {ty1 -> (... (tyn -> ty) ...)}, then
{strip_fun fty} returns {([ty1,...,tyn],ty)}. Note that

   strip_fun(list_mk_fun([ty1,...,tyn],ty))

will not return {([ty1,...,tyn],ty)} if {ty} is a function type.

FAILURE
Never fails.

EXAMPLE

- strip_fun (Type `:(a -> 'bool) -> ('b -> 'c)`);
> val it = ([`:a -> 'bool`, `:'b`], `:'c`) : hol_type list * hol_type


SEEALSO
boolSyntax.list_mk_fun, Type.dom_rng, Type.dest_type.

----------------------------------------------------------------------