strip_gabs : term -> term list * term

SYNOPSIS

Breaks apart an iterated generalized or basic abstraction.

DESCRIPTION

If the term t is iteratively constructed by basic or generalized abstractions, i.e. is of the form \vs1. \vs2. ... \vsn. t, then the call strip_gabs t returns a pair of the list of varstructs and the term [vs1; vs2; ...; vsn],t.

FAILURE CONDITIONS

Never fails, though the list of varstructs will be empty if the initial term is no sort of abstraction.

EXAMPLE

  # strip_gabs `\(a,b) c ((d,e),f). (a - b) + c + (d - e) * f`;;
  val it : term list * term =
    ([`a,b`; `c`; `(d,e),f`], `a - b + c + (d - e) * f`)

SEE ALSO

dest_gabs, is_gabs, mk_gabs.