strip_abs : term -> term list * term
STRUCTURE
SYNOPSIS
Break apart consecutive lambda abstractions.
DESCRIPTION
If M is a term of the form \v1...vn.N, where N is not a lambda abstraction, then strip_abs M equals ([v1,...,vn],N). Otherwise, the result is ([],M).
FAILURE
Never fails.
EXAMPLE
- strip_abs (Term `\x y z. x ==> y ==> z`);
> val it = ([`x`, `y`, `z`], `x ==> y ==> z`) : term list * term

- strip_abs T;
> val it = ([], `T`) : term list * term

COMMENTS
In the current implementation of HOL, strip_abs is far faster than iterating dest_abs for terms with many consecutive binders.
SEEALSO
HOL  Kananaskis-14