dest_binder : string -> term -> term * term

- SYNOPSIS
- Breaks apart a ``binder''.
- DESCRIPTION
- Applied to a term tm of the form `c (\x. t)` where c is a constant whose name is "s", the call dest_binder "c" tm returns (`x`,`t`). Note that this is actually independent of whether the name parses as a binder, but the usual application is where it does.
- FAILURE CONDITIONS
- Fails if the term is not of the appropriate form with a constant of the same name.
- EXAMPLE
- The call dest_binder "!" is the same as dest_forall, and is in fact how that function is implemented.
- SEE ALSO
- dest_abs, dest_comb, dest_const, dest_var.