dest_abs

Term.dest_abs : term -> term * term

Breaks apart an abstraction into abstracted variable and body.

dest_abs is a term destructor for abstractions: if M is a term of the form \v.t, then dest_abs M returns (v,t).

Failure

Fails if it is not given a lambda abstraction.

See also

Term.mk_abs, Term.is_abs, Term.dest_var, Term.dest_const, Term.dest_comb, boolSyntax.strip_abs