@@ -8,6 +8,7 @@ import Prelude.Applicative
88import Prelude.Monad
99import Prelude.Nat
1010import Prelude.List
11+import Prelude.Foldable
1112
1213%access public export
1314%default total
@@ -109,6 +110,12 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
109110 cycle' [] = x :: cycle' xs
110111 cycle' (y :: ys) = y :: cycle' ys
111112
113+||| Produce a Stream that is prefixed by elements from a Foldable
114+||| @ pfx the Foldable containing elements to prepend
115+||| @ stream the Stream to prepend the elements to
116+startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a
117+startWith pfx stream = foldr (\x, xs => x :: xs) stream pfx
118+
112119Applicative Stream where
113120 pure = repeat
114121 (<*>) = zipWith apply