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
31
32
33
|
\DOC rev_splitlist
\TYPE {rev_splitlist : ('a -> 'a * 'b) -> 'a -> 'a * 'b list}
\SYNOPSIS
Applies a binary destructor repeatedly in right-associative mode.
\DESCRIBE
If a destructor function {d} inverts a binary constructor {f}, for example
{dest_comb} for {mk_comb}, and fails when applied to {y}, then:
{
rev_splitlist d f(...(f(f(w,x1),x2),...xn)
}
\noindent returns
{
(w,[x1; ... ; xn])
}
\FAILURE
Never fails.
\EXAMPLE
The function {strip_comb} is actually just defined as
{rev_splitlist dest_comb}, which acts as follows:
{
# rev_splitlist dest_comb `x + 1 + 2`;;
val it : term * term list = (`(+)`, [`x`; `1 + 2`])
}
\SEEALSO
itlist, nsplit, splitlist, striplist.
\ENDDOC
|
