first : ('a -> bool) -> 'a list -> 'a
STRUCTURE
SYNOPSIS
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  ""

SEEALSO
HOL  Kananaskis-14