src/Pure/library.ML
changeset 31986 a68f88d264f7
parent 31250 4b99b1214034
child 32188 005f9abae1e3
equal deleted inserted replaced
31985:a6e982b1ebba 31986:a68f88d264f7
    95   val nth_list: 'a list list -> int -> 'a list
    95   val nth_list: 'a list list -> int -> 'a list
    96   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    96   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    97   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    97   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    98   val split_last: 'a list -> 'a list * 'a
    98   val split_last: 'a list -> 'a list * 'a
    99   val find_index: ('a -> bool) -> 'a list -> int
    99   val find_index: ('a -> bool) -> 'a list -> int
   100   val find_index_eq: ''a -> ''a list -> int
       
   101   val find_first: ('a -> bool) -> 'a list -> 'a option
   100   val find_first: ('a -> bool) -> 'a list -> 'a option
   102   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   101   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   103   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   102   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   104   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   103   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   105   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   104   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   501 fun find_index pred =
   500 fun find_index pred =
   502   let fun find (_: int) [] = ~1
   501   let fun find (_: int) [] = ~1
   503         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   502         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   504   in find 0 end;
   503   in find 0 end;
   505 
   504 
   506 fun find_index_eq x = find_index (equal x);
       
   507 
       
   508 (*find first element satisfying predicate*)
   505 (*find first element satisfying predicate*)
   509 val find_first = List.find;
   506 val find_first = List.find;
   510 
   507 
   511 (*get first element by lookup function*)
   508 (*get first element by lookup function*)
   512 fun get_first _ [] = NONE
   509 fun get_first _ [] = NONE