@@ -3,7 +3,7 @@ module Data.Stream.Extra
3%access public export
3%access public export
4%default total
4%default total
6−||| Produce a Stream that is prefixed by elements from a Foldable
6+||| Insert elements from a Foldable at the start of an existing Stream
7||| @ pfx the Foldable containing elements to prepend
7||| @ pfx the Foldable containing elements to prepend
8||| @ stream the Stream to prepend the elements to
8||| @ stream the Stream to prepend the elements to
9startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a
9startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a