strip_fun

boolSyntax.strip_fun : hol_type -> hol_type list * hol_type

Iteratively breaks apart function types.

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)`);
Exception- HOL_ERR
  (at Parse.type parser: at line 1, character 19:
       a not a known type operator) raised

See also

boolSyntax.list_mk_fun, Type.dom_rng, Type.dest_type