Constructs an instance of a named monomorphic binary operator.
DESCRIPTION
The call mk_binary s (l,r) constructs a binary application (op l) r where
op is the monomorphic constant with name s. Note that it will in general
not work if the constant is polymorphic.
FAILURE CONDITIONS
If there is no constant at all with name s, or if the constant is polymorphic
and the terms do not match its most general type.
EXAMPLE
This case works fine:
# mk_binary "+" (`1`,`2`);;
val it : term = `1 + 2`
but here we hit the monomorphism restriction:
# mk_binary "=" (`a:A`,`b:A`);;
val it : term = `a = b`
# mk_binary "=" (`1`,`2`);;
Exception: Failure "mk_binary".