1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\DOC mk_binop
\TYPE {mk_binop : term -> term -> term -> term}
\SYNOPSIS
The call {mk_binop op l r} returns the term {(op l) r}.
\KEYWORDS
\LIBRARY
\DESCRIBE
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
Fails if the types are incompatible.
\EXAMPLE
{
# mk_binop `(+):num->num->num` `1` `2`;;
val it : term = `1 + 2`
}
\SEEALSO
dest_binop, is_binop, mk_binary.
\ENDDOC
|
