dest_abs : term -> term * term

SYNOPSIS

Breaks apart an abstraction into abstracted variable and body.

DESCRIPTION

dest_abs is a term destructor for abstractions: dest_abs `\var. t` returns (`var`,`t`).

FAILURE CONDITIONS

Fails with dest_abs if term is not an abstraction.

EXAMPLE

  # dest_abs `\x. x + 1`;;
  val it : term * term = (`x`, `x + 1`)

SEE ALSO

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