- cantor : Stream (Stream a) -> Stream a
- Totality: total
- cycle : (xs : List a) -> {auto 0 _ : NonEmpty xs} -> Stream a
Produce a Stream repeating a sequence
@ xs the sequence to repeat
@ ok proof that the list is non-empty
Totality: total- diag : Stream (Stream a) -> Stream a
Return the diagonal elements of a stream of streams
Totality: total- drop : Nat -> Stream a -> Stream a
Drop the first n elements from the stream
@ n how many elements to drop
Totality: total- index : Nat -> Stream a -> a
Get the nth element of a stream
Totality: total- iterate : (a -> a) -> 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
Totality: total- nats : Stream Nat
All of the natural numbers, in order
Totality: total- repeat : a -> Stream a
An infinite stream of repetitions of the same thing
Totality: total- scanl : (a -> b -> a) -> a -> 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
Totality: total- unfoldr : (b -> (a, b)) -> b -> Stream a
- Totality: total
- zag : List1 a -> List1 (Stream a) -> Stream (Stream a) -> Stream a
- Totality: total
- zig : List1 (Stream a) -> Stream (Stream a) -> Stream a
- Totality: total
- zipWith3IndexLinear : (0 f : (a -> a -> a -> a)) -> (xs : Stream a) -> (ys : Stream a) -> (zs : Stream a) -> (i : Nat) -> index i (zipWith3 f xs ys zs) = f (index i xs) (index i ys) (index i zs)
- Totality: total
- zipWithIndexLinear : (0 f : (a -> a -> a)) -> (xs : Stream a) -> (ys : Stream a) -> (i : Nat) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)
- Totality: total