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

See also

Lib.first, Lib.filter, Lib.mapfilter, Lib.tryfind