src/Pure/General/seq.ML
changeset 8535 7428194b39f7
parent 6927 83759063fbbd
child 8806 a202293db3f6
     1.1 --- a/src/Pure/General/seq.ML	Mon Mar 20 18:45:28 2000 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Mon Mar 20 18:46:53 2000 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
     1.5    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
     1.6    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
     1.7 +  val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
     1.8  end;
     1.9  
    1.10  structure Seq: SEQ =
    1.11 @@ -217,4 +218,9 @@
    1.12  fun REPEAT1 f = THEN (f, REPEAT f);
    1.13  
    1.14  
    1.15 +fun INTERVAL f i j x =
    1.16 +  if i > j then single x
    1.17 +  else op THEN (f j, INTERVAL f i (j - 1)) x;
    1.18 +
    1.19 +
    1.20  end;