get_first: ('a -> 'b option) -> 'a list -> 'b option;
authorwenzelm
Wed May 13 12:17:30 1998 +0200 (1998-05-13)
changeset 4916fe8b0c82691b
parent 4915 5ff99bd60da9
child 4917 7c22890a7a9b
get_first: ('a -> 'b option) -> 'a list -> 'b option;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed May 13 10:21:28 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Wed May 13 12:17:30 1998 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4    val find_index: ('a -> bool) -> 'a list -> int
     1.5    val find_index_eq: ''a -> ''a list -> int
     1.6    val find_first: ('a -> bool) -> 'a list -> 'a option
     1.7 +  val get_first: ('a -> 'b option) -> 'a list -> 'b option
     1.8    val flat: 'a list list -> 'a list
     1.9    val seq: ('a -> unit) -> 'a list -> unit
    1.10    val separate: 'a -> 'a list -> 'a list
    1.11 @@ -471,6 +472,13 @@
    1.12    | find_first pred (x :: xs) =
    1.13        if pred x then Some x else find_first pred xs;
    1.14  
    1.15 +(*get first element by lookup function*)
    1.16 +fun get_first _ [] = None
    1.17 +  | get_first f (x :: xs) =
    1.18 +      (case f x of
    1.19 +        None => get_first f xs
    1.20 +      | some => some);
    1.21 +
    1.22  (*flatten a list of lists to a list*)
    1.23  fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
    1.24