git.iko.soy/Idris-dev
on master help sign in
move `startWith` from prelude to contrib
commit51a637923481d6f5d822a09451d4f53b367c1ddb authorMichael Morgan <morgan.michael@me.com> dateWed 23 Aug 2017, 14:51 (9 years ago) parent9c56c15
3 files changed+13−9
compare with master
unifiedsplit
libs/contrib/Data/Stream/Extra.idr+10 libs/contrib/contrib.ipkg+3−2 libs/prelude/Prelude/Stream.idr−7
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+||| Produce a Stream that is prefixed by elements from a Foldable
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
libs/prelude/Prelude/Stream.idr−7
@@ -8,7 +8,6 @@ import Prelude.Applicative
88import Prelude.Monad
99import Prelude.Nat
1010import Prelude.List
11−import Prelude.Foldable
1211
1312%access public export
1413%default total
@@ -110,12 +109,6 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
110109 cycle' [] = x :: cycle' xs
111110 cycle' (y :: ys) = y :: cycle' ys
112111
113−||| Produce a Stream that is prefixed by elements from a Foldable
114−||| @ pfx the Foldable containing elements to prepend
115−||| @ stream the Stream to prepend the elements to
116−startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a
117−startWith pfx stream = foldr (\x, xs => x :: xs) stream pfx
118−
119112Applicative Stream where
120113 pure = repeat
121114 (<*>) = zipWith apply