trypluck
Lib.trypluck : ('a -> 'b) -> 'a list -> 'b * 'a list
Pull an element out of a list.
An invocation trypluck f [x1,...,xk,...,xn] returns a pair
(f(xk),[x1,...,xk-1,xk+1,...xn])
where xk has been lifted out of the list without disturbing the
relative positions of the other elements. For this to happen, f(xk)
must hold, and f(xi) must fail for x1,...,xk-1.
Failure
If the input list is empty. Also fails if f fails on every member of
the list.
Example
> val (x,rst) = trypluck BETA_CONV [``1``,``(\x. x+2) 3``, ``p + q``];
val rst = [“1”, “p + q”]: term list
val x = ⊢ (λx. x + 2) 3 = 3 + 2: thm