git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4016 from msmorgan/feature/stream-startWith

add startWith function for prepending a finite number of elements to a Stream

commit33bff54d62169903cba0ab407c85ac00f1aa11c4 authorNiklas Larsson <metaniklas@gmail.com> dateThu 24 Aug 2017, 19:07 (9 years ago) parentf83cc0d6dbef7a
2 files changed+13−2
compare with master
unifiedsplit
libs/contrib/Data/Stream/Extra.idr+10 libs/contrib/contrib.ipkg+3−2
libs/contrib/Data/Stream/Extra.idrnew file+10
@@ -0,0 +1,10 @@
1+module Data.Stream.Extra
2+
3+%access public export
4+%default total
5+
6+||| Insert elements from a Foldable at the start of an existing Stream
7+||| @ pfx the Foldable containing elements to prepend
8+||| @ stream the Stream to prepend the elements to
9+startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a
10+startWith pfx stream = foldr (\x, xs => x :: xs) stream pfx
libs/contrib/contrib.ipkg+3−2
@@ -22,7 +22,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
2222 Data.Heap,
2323 Data.SortedMap, Data.SortedSet,
2424 Data.CoList, Data.Storable,
25− Data.List.Zipper,
25+ Data.List.Zipper,
2626
2727 Decidable.Decidable, Decidable.Order,
2828
@@ -39,4 +39,5 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
3939
4040 Text.Literate,
4141
42− Data.Fin.Extra
42+ Data.Fin.Extra,
43+ Data.Stream.Extra