@@ -67,4 +67,31 @@ unzip xs = (map fst xs, map snd xs)
6767diag : Stream (Stream a) -> Stream a
6868diag ((x::xs)::xss) = x :: diag (map tail xss)
6969
70+||| Fold a Stream corecursively. Since there is no Nil, no initial value is used.
71+||| @ f the combining function
72+||| @ xs the Stream to fold up
73+foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b
74+foldr f (x :: xs) = f x (foldr f xs)
75+
76+||| Produce a Stream of left folds of prefixes of the given Stream
77+||| @ f the combining function
78+||| @ acc the initial value
79+||| @ xs the Stream to process
80+scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a
81+scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
82+
83+||| Produce a Stream of (corecursive) right folds of tails of the given Stream
84+||| @ f the combining function
85+||| @ xs the Stream to fold up
86+-- Reusing the head of the corecursion in the obvious way doesn’t productivity check
87+scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b
88+scanr f (x :: Delay xs) = f x (foldr f xs) :: scanr f xs
89+
90+||| Produce a Stream repeating a sequence
91+||| @ xs the sequence to repeat
92+cycle : (xs : Vect (S n) a) -> Stream a
93+cycle xs = cycle_ xs xs
94+ where cycle_ : Vect (S n) a -> Vect m a -> Stream a
95+ cycle_ (x :: xs) [] = x :: cycle_ (x :: xs) xs
96+ cycle_ xs (x :: ys) = x :: cycle_ xs ys
7097