added nth_update: 'a -> int * 'a list -> 'a list;
authorwenzelm
Mon May 04 21:05:38 1998 +0200 (1998-05-04)
changeset 4893df9d6eef16d5
parent 4892 0f80e924009d
child 4894 32187e0b8b48
added nth_update: 'a -> int * 'a list -> 'a list;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon May 04 21:05:14 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Mon May 04 21:05:38 1998 +0200
     1.3 @@ -80,6 +80,7 @@
     1.4    val nth_elem: int * 'a list -> 'a
     1.5    val last_elem: 'a list -> 'a
     1.6    val split_last: 'a list -> 'a list * 'a
     1.7 +  val nth_update: 'a -> int * 'a list -> 'a list
     1.8    val find_index: ('a -> bool) -> 'a list -> int
     1.9    val find_index_eq: ''a -> ''a list -> int
    1.10    val find_first: ('a -> bool) -> 'a list -> 'a option
    1.11 @@ -446,6 +447,17 @@
    1.12    | split_last [x] = ([], x)
    1.13    | split_last (x :: xs) = apfst (cons x) (split_last xs);
    1.14  
    1.15 +(*update nth element*)
    1.16 +fun nth_update x (n, xs) =
    1.17 +  let
    1.18 +    val prfx = take (n, xs);
    1.19 +    val sffx = drop (n, xs);
    1.20 +  in
    1.21 +    (case sffx of
    1.22 +      [] => raise LIST "nth_update"
    1.23 +    | _ :: sffx' => prfx @ (x :: sffx'))
    1.24 +  end;
    1.25 +
    1.26  (*find the position of an element in a list*)
    1.27  fun find_index pred =
    1.28    let fun find _ [] = ~1