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