improve documentation for Data.Stream.Extra.startWith
commit6dbef7aee71d061ff0d353999a05650128724447
authorMichael Morgan <morgan.michael@me.com>
dateWed 23 Aug 2017, 15:05 (9 years ago)
parent51a6379
libs/contrib/Data/Stream/Extra.idr+1−1
@@ -3,7 +3,7 @@ module Data.Stream.Extra
33%access public export
44%default total
55
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
77||| @ pfx the Foldable containing elements to prepend
88||| @ stream the Stream to prepend the elements to
99startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a