mk_binary : string -> term * term -> term
Constructs an instance of a named monomorphic binary operator.
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.
This case works fine:
but here we hit the monomorphism restriction:
# mk_binary "+" (`1`,`2`);;
val it : term = `1 + 2`
# mk_binary "=" (`a:A`,`b:A`);;
val it : term = `a = b`
# mk_binary "=" (`1`,`2`);;
Exception: Failure "mk_binary".
- SEE ALSO
dest_binary, is_binary, mk_binop.