strip_abs

Term.strip_abs : term -> term list * term

Also exported as boolSyntax.strip_abs.

Break apart consecutive lambda abstractions.

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.

See also

Term.strip_binder, Term.dest_abs, boolSyntax.strip_forall, boolSyntax.strip_exists