dest_binary : string -> term -> term * term
Breaks apart an instance of a binary operator with given name.
The call dest_binary s tm will, if tm is a binary operator application
(op l) r where op is a constant with name s, return the two arguments to
which it is applied as a pair l,r. Otherwise, it fails. Note that op is
required to be a constant.
- FAILURE CONDITIONS
This one succeeds:
# dest_binary "+" `1 + 2`;;
val it : term * term = (`1`, `2`)
- SEE ALSO
dest_binop, is_binary, is_comb, mk_binary.