0 | module Data.Stream.Extra 1 | 2 | %default total 3 | 4 | ||| Insert elements from a Foldable at the start of an existing Stream 5 | ||| @ pfx the Foldable containing elements to prepend 6 | ||| @ stream the Stream to prepend the elements to 7 | public export 8 | startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a 9 | startWith pfx stream = foldr (\x, xs => x :: xs) stream pfx 10 |