mk_binop : term -> term -> term -> term
The call mk_binop op l r returns the term (op l) r.
The call mk_binop op l r returns the term (op l) r provided that is
well-typed. Otherwise it fails. The term op need not be a constant nor parsed
as infix, but that is the usual case. Note that type variables in op are not
instantiated, so it needs to be the correct instance for the terms l and r.
- FAILURE CONDITIONS
Fails if the types are incompatible.
# mk_binop `(+):num->num->num` `1` `2`;;
val it : term = `1 + 2`
- SEE ALSO
dest_binop, is_binop, mk_binary.