trypluck : ('a -> 'b) -> 'a list -> 'b * 'a list
STRUCTURE
SYNOPSIS
Pull an element out of a list.
DESCRIPTION
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
SEEALSO
HOL  Kananaskis-13