map_nth_elem;
authorwenzelm
Mon Oct 15 20:31:18 2001 +0200 (2001-10-15)
changeset 11773983d2db52062
parent 11772 cf618fe8facd
child 11774 3bc4f67d7fe1
map_nth_elem;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Oct 15 17:02:57 2001 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Oct 15 20:31:18 2001 +0200
     1.3 @@ -91,6 +91,7 @@
     1.4    val drop: int * 'a list -> 'a list
     1.5    val dropwhile: ('a -> bool) -> 'a list -> 'a list
     1.6    val nth_elem: int * 'a list -> 'a
     1.7 +  val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
     1.8    val last_elem: 'a list -> 'a
     1.9    val split_last: 'a list -> 'a list * 'a
    1.10    val nth_update: 'a -> int * 'a list -> 'a list
    1.11 @@ -508,6 +509,10 @@
    1.12      [] => raise LIST "nth_elem"
    1.13    | x :: _ => x);
    1.14  
    1.15 +fun map_nth_elem 0 f (x :: xs) = f x :: xs
    1.16 +  | map_nth_elem n f (x :: xs) = x :: map_nth_elem (n - 1) f xs
    1.17 +  | map_nth_elem _ _ [] = raise LIST "map_nth_elem";
    1.18 +
    1.19  (*last element of a list*)
    1.20  fun last_elem [] = raise LIST "last_elem"
    1.21    | last_elem [x] = x