rev_splitlist : ('a -> 'a * 'b) -> 'a -> 'a * 'b list
- SYNOPSIS
-
Applies a binary destructor repeatedly in right-associative mode.
- DESCRIPTION
-
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)
- FAILURE CONDITIONS
-
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`])
- SEE ALSO
-
itlist, nsplit, splitlist, striplist.