git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4016 from msmorgan/feature/stream-startWith
33bff54Niklas Larsson
libs/contrib/Data/Stream/Extra.idrnew file+10
compare with master
unifiedsplit
@@ -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,
22 Data.Heap,
22 Data.Heap,
23 Data.SortedMap, Data.SortedSet,
23 Data.SortedMap, Data.SortedSet,
24 Data.CoList, Data.Storable,
24 Data.CoList, Data.Storable,
25− Data.List.Zipper,
25+ Data.List.Zipper,
26
26
27 Decidable.Decidable, Decidable.Order,
27 Decidable.Decidable, Decidable.Order,
28
28
@@ -39,4 +39,5 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
39
39
40 Text.Literate,
40 Text.Literate,
41
41
42− Data.Fin.Extra
42+ Data.Fin.Extra,
43+ Data.Stream.Extra