src/Pure/library.ML
changeset 19233 77ca20b0ed77
parent 19119 dea8d858d37f
child 19273 05b6d220e509
     1.1 --- a/src/Pure/library.ML	Fri Mar 10 12:28:38 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Mar 10 15:33:48 2006 +0100
     1.3 @@ -126,6 +126,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_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
     1.8    val get_first: ('a -> 'b option) -> 'a list -> 'b option
     1.9    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    1.10    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    1.11 @@ -632,6 +633,15 @@
    1.12          NONE => get_first f xs
    1.13        | some => some);
    1.14  
    1.15 +fun get_index f =
    1.16 +  let
    1.17 +    fun get _ [] = NONE
    1.18 +      | get i (x::xs) = 
    1.19 +          case f x
    1.20 +           of NONE => get (i+1) xs
    1.21 +            | SOME y => SOME (i, y)
    1.22 +  in get 0 end;
    1.23 +
    1.24  (*flatten a list of lists to a list*)
    1.25  val flat = List.concat;
    1.26