1\DOC first
2
3\TYPE {first : ('a -> bool) -> 'a list -> 'a}
4
5\SYNOPSIS
6Return first element in list that predicate holds of.
7
8\KEYWORDS
9list, predicate, search
10
11\DESCRIBE
12An invocation {first P [x1,...,xk,...xn]} returns {xk} if {P xk} returns
13{true} and {P xi (1 <= i < k)} equals {false}.
14
15\FAILURE
16If {P xi} is {false} for every element in {list}, then {first P list} raises
17an exception. When searching for an element of {list} that {P} holds of, it
18may happen that an application of {P} to an element of {list} raises an
19exception {e}. In that case, {first P list} also raises {e}.
20
21\EXAMPLE
22{
23- first (fn i => i mod 2 = 0) [1,3,4,5];
24> val it = 4 : int
25
26- first (fn i => i mod 2 = 0) [1,3,5,7];
27! Uncaught exception:
28! HOL_ERR
29
30- first (fn _ => raise Fail "") [1];
31! Uncaught exception:
32! Fail  ""
33}
34
35
36\SEEALSO
37Lib.exists, Lib.tryfind, Lib.all.
38\ENDDOC
39