@@ -8,6 +8,7 @@ import Prelude.Applicative
8import Prelude.Monad
8import Prelude.Monad
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.List
10import Prelude.List
11+import Prelude.Foldable
12%access public export
13%access public export
13%default total
14%default total
@@ -109,6 +110,12 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
109 cycle' [] = x :: cycle' xs
110 cycle' [] = x :: cycle' xs
110 cycle' (y :: ys) = y :: cycle' ys
111 cycle' (y :: ys) = y :: cycle' ys
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
112Applicative Stream where
119Applicative Stream where
113 pure = repeat
120 pure = repeat
114 (<*>) = zipWith apply
121 (<*>) = zipWith apply