src/Pure/library.ML
changeset 33063 4d462963a7db
parent 33050 fe166e8b9f07
child 33073 2f6ce3b9ec39
child 33078 3aea60ca3900
     1.1 --- a/src/Pure/library.ML	Thu Oct 22 10:52:07 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Oct 22 13:48:06 2009 +0200
     1.3 @@ -89,6 +89,7 @@
     1.4    val nth_list: 'a list list -> int -> 'a list
     1.5    val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
     1.6    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.7 +  val map_range: (int -> 'a) -> int -> 'a list
     1.8    val split_last: 'a list -> 'a list * 'a
     1.9    val find_index: ('a -> bool) -> 'a list -> int
    1.10    val find_first: ('a -> bool) -> 'a list -> 'a option
    1.11 @@ -463,6 +464,12 @@
    1.12        | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
    1.13    in fold_aux 0 end;
    1.14  
    1.15 +fun map_range f i =
    1.16 +  let
    1.17 +    fun mapp k =
    1.18 +      if k < i then f k :: mapp (k + 1) else [];
    1.19 +  in mapp 0 end;
    1.20 +
    1.21  val last_elem = List.last;
    1.22  
    1.23  (*rear decomposition*)