dest_binop : term -> term -> term * term
Breaks apart an application of a given binary operator to two arguments.
The call dest_binop op t, where t is of the form (op l) r, will return
the pair l,r. If t is not of that form, it fails. Note that op can be any
term; it need not be a constant nor parsed infix.
- FAILURE CONDITIONS
Fails if the term is not a binary application of operator op.
# dest_binop `(+):num->num->num` `1 + 2 + 3`;;
val it : term * term = (`1`, `2 + 3`)
- SEE ALSO
dest_binary, is_binary, is_binop, mk_binary, mk_binop.