Prelude.Stream

data Stream : Type -> Type

An infinite stream

(::) : (value : elem) -> Inf (Stream elem) -> Stream elem

Fixity

Left associative, precedence 7

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

Produce a Stream repeating a sequence

xs

the sequence to repeat

ok

proof that the list is non-empty

diag : Stream (Stream a) -> Stream a

Return the diagonal elements of a stream of streams

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

Drop the first n elements from the stream

n

how many elements to drop

head : Stream a -> a

The first element of an infinite stream

index : Nat -> Stream a -> a

Get the nth element of a stream

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

Generate an infinite stream by repeatedly applying a function

f

the function to iterate

x

the initial value that will be the head of the stream

repeat : a -> Stream a

An infinite stream of repetitions of the same thing

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

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

f

the combining function

acc

the initial value

xs

the Stream to process

tail : Stream a -> Stream a

All but the first element

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

Take precisely n elements from the stream

n

how many elements to take

xs

the stream

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

Create a pair of streams from a stream of pairs

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

Split a stream of three-element tuples into three streams

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

Create a stream of pairs from two streams

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

Combine three streams into a stream of tuples elementwise

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

Combine two streams element-wise using a function.

f

the function to combine elements with

xs

the first stream of elements

ys

the second stream of elements

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

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