Return first element in list that predicate holds of.
DESCRIPTION
An invocation first P [x1,...,xk,...xn] returns xk if P xk returns
true and P xi (1 <= i < k) equals false.
FAILURE
If P xi is false for every element in list, then first P list raises
an exception. When searching for an element of list that P holds of, it
may happen that an application of P to an element of list raises an
exception e. In that case, first P list also raises e.
EXAMPLE
- first (fn i => i mod 2 = 0) [1,3,4,5];
> val it = 4 : int
- first (fn i => i mod 2 = 0) [1,3,5,7];
! Uncaught exception:
! HOL_ERR
- first (fn _ => raise Fail "") [1];
! Uncaught exception:
! Fail ""