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.