mk_binop : term -> term -> term -> term

SYNOPSIS

The call mk_binop op l r returns the term (op l) r. \LIBRARY

DESCRIPTION

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.

EXAMPLE

  # mk_binop `(+):num->num->num` `1` `2`;;
  val it : term = `1 + 2`

SEE ALSO

dest_binop, is_binop, mk_binary.