@@ -109,6 +109,15 @@ partial -- and the call to foldr isn't guarded anyway!
109109scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b
110110scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs
111111
112+||| Produce a Stream repeating a sequence
113+||| @ xs the sequence to repeat
114+||| @ ok proof that the list is non-empty
115+cycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream a
116+cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
117+ where cycle' : List a -> Stream a
118+ cycle' [] = x :: cycle' xs
119+ cycle' (y :: ys) = y :: cycle' ys
120+
112121instance Applicative Stream where
113122 pure = repeat
114123 (<*>) = zipWith apply