51a6379 · Idris-dev · git.iko.soy

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+||| 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,

22 Data.Heap,

23 Data.SortedMap, Data.SortedSet,

24 Data.CoList, Data.Storable,

25− Data.List.Zipper,

25+ Data.List.Zipper,

26

27 Decidable.Decidable, Decidable.Order,

28

@@ -39,4 +39,5 @@ modules = CFFI, CFFI.Types, CFFI.Memory,

39

40 Text.Literate,

41

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

8import Prelude.Monad

9import Prelude.Nat

10import Prelude.List

11−import Prelude.Foldable

12

11

13%access public export

12%access public export

14%default total

13%default total

@@ -110,12 +109,6 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs

110 cycle' [] = x :: cycle' xs

109 cycle' [] = x :: cycle' xs

111 cycle' (y :: ys) = y :: cycle' ys

110 cycle' (y :: ys) = y :: cycle' ys

112

111

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−

119Applicative Stream where

112Applicative Stream where

120 pure = repeat

113 pure = repeat

121 (<*>) = zipWith apply

114 (<*>) = zipWith apply