IdrisDoc: Prelude.Stream


zipWith3 : (a -> b -> c -> d) -> Stream a -> Stream b -> Stream c -> Stream d

Combine three streams by applying a function element-wise along them

zipWith : (f : a -> b -> c) -> (xs : Stream a) -> (ys : Stream b) -> Stream c

Combine two streams element-wise using a function.


the function to combine elements with


the first stream of elements


the second stream of elements

zip3 : Stream a -> Stream b -> Stream c -> Stream (a, b, c)

Combine three streams into a stream of tuples elementwise

zip : Stream a -> Stream b -> Stream (a, b)

Create a stream of pairs from two streams

unzip3 : Stream (a, b, c) -> (Stream a, Stream b, Stream c)

Split a stream of three-element tuples into three streams

unzip : Stream (a, b) -> (Stream a, Stream b)

Create a pair of streams from a stream of pairs

take : (n : Nat) -> (xs : Stream a) -> List a

Take precisely n elements from the stream


how many elements to take


the stream

tail : Stream a -> Stream a

All but the first element

scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a

Produce a Stream of left folds of prefixes of the given Stream


the combining function


the initial value


the Stream to process

repeat : a -> Stream a

An infinite stream of repetitions of the same thing

iterate : (f : a -> a) -> (x : a) -> Stream a

Generate an infinite stream by repeatedly applying a function


the function to iterate


the initial value that will be the head of the stream

index : Nat -> Stream a -> a

Get the nth element of a stream

head : Stream a -> a

The first element of an infinite stream

drop : (n : Nat) -> Stream a -> Stream a

Drop the first n elements from the stream


how many elements to drop

diag : Stream (Stream a) -> Stream a

Return the diagonal elements of a stream of streams

cycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream a

Produce a Stream repeating a sequence


the sequence to repeat


proof that the list is non-empty

data Stream : Type -> Type

An infinite stream

(::) : (value : elem) -> Inf (Stream elem) -> Stream elem
Left associative, precedence 7