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
|
\DOC dest_binop
\TYPE {dest_binop : term -> term -> term * term}
\SYNOPSIS
Breaks apart an application of a given binary operator to two arguments.
\DESCRIBE
The call {dest_binop op t}, where {t} is of the form {(op l) r}, will return
the pair {l,r}. If {t} is not of that form, it fails. Note that {op} can be any
term; it need not be a constant nor parsed infix.
\FAILURE
Fails if the term is not a binary application of operator {op}.
\EXAMPLE
{
# dest_binop `(+):num->num->num` `1 + 2 + 3`;;
val it : term * term = (`1`, `2 + 3`)
}
\SEEALSO
dest_binary, is_binary, is_binop, mk_binary, mk_binop.
\ENDDOC
|
