strip_abs : term -> term list * term

SYNOPSIS

Iteratively breaks apart abstractions.

DESCRIPTION

strip_abs `\x1 ... xn. t` returns ([`x1`;...;`xn`],`t`). Note that

   strip_abs(list_mk_abs([`x1`;...;`xn`],`t`))

will not return ([`x1`;...;`xn`],`t`) if t is an abstraction.

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # strip_abs `\x y z. x /\ y /\ z`;;
  val it : term list * term = ([`x`; `y`; `z`], `x /\ y /\ z`)

SEE ALSO

list_mk_abs, dest_abs.