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 x = |- (\x. x + 2) 3 = 3 + 2 : thm
val rst = [``1``, ``p + q``] : term list