dest_gabs : term -> term * term
Breaks apart a generalized abstraction into abstracted varstruct and body.
dest_pabs is a term destructor for generalized abstractions: for example with
a paired varstruct the effect on dest_pabs `\(v1..(..)..vn). t` is to return
the pair (`(v1..(..)..vn)`,`t`). It will also act as for dest_abs on basic
- FAILURE CONDITIONS
Fails unless the term is a basic or generalized abstraction.
These are fairly typical applications:
while the following shows that it also works on basic abstractions:
# dest_gabs `\(x,y). x + y`;;
val it : term * term = (`x,y`, `x + y`)
# dest_gabs `\(CONS h t). h + 1`;;
val it : term * term = (`CONS h t`, `h + 1`)
# dest_gabs `\x. x`;;
Warning: inventing type variables
val it : term * term = (`x`, `x`)
- SEE ALSO
GEN_BETA_CONV, is_gabs, mk_gabs, strip_gabs.