Idris2Doc : Data.Stream

Data.Stream

cantor : Stream (Streama) -> Streama
Totality: total
cycle : (xs : Lista) -> {auto 0 _ : NonEmptyxs} -> Streama
  Produce a Stream repeating a sequence
@ xs the sequence to repeat
@ ok proof that the list is non-empty

Totality: total
diag : Stream (Streama) -> Streama
  Return the diagonal elements of a stream of streams

Totality: total
drop : Nat -> Streama -> Streama
  Drop the first n elements from the stream
@ n how many elements to drop

Totality: total
index : Nat -> Streama -> a
  Get the nth element of a stream

Totality: total
iterate : (a -> a) -> a -> Streama
  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 : StreamNat
  All of the natural numbers, in order

Totality: total
repeat : a -> Streama
  An infinite stream of repetitions of the same thing

Totality: total
scanl : (a -> b -> a) -> a -> Streamb -> Streama
  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 -> Streama
Totality: total
zag : List1a -> List1 (Streama) -> Stream (Streama) -> Streama
Totality: total
zig : List1 (Streama) -> Stream (Streama) -> Streama
Totality: total
zipWith3IndexLinear : (0 f : (a -> a -> a -> a)) -> (xs : Streama) -> (ys : Streama) -> (zs : Streama) -> (i : Nat) -> indexi (zipWith3fxsyszs) = f (indexixs) (indexiys) (indexizs)
Totality: total
zipWithIndexLinear : (0 f : (a -> a -> a)) -> (xs : Streama) -> (ys : Streama) -> (i : Nat) -> indexi (zipWithfxsys) = f (indexixs) (indexiys)
Totality: total