rev_splitlist : ('a -> 'a * 'b) -> 'a -> 'a * 'b list
Applies a binary destructor repeatedly in right-associative mode.
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
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.