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 pairwhere 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.
(f(xk),[x1,...,xk-1,xk+1,...xn])

- 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-14