strip_gabs : term -> term list * term
Breaks apart an iterated generalized or basic abstraction.
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.
# 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.