Data.Stream

Reexports

Definitions

drop : Nat -> Stream a -> Stream a

  Drop the first n elements from the stream
  @ n how many elements to drop

Totality: total
Visibility: public export

repeat : a -> Stream a

  An infinite stream of repetitions of the same thing

Totality: total
Visibility: public export

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
Visibility: public export

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

Totality: total
Visibility: public export

nats : Stream Nat

  All of the natural numbers, in order

Totality: total
Visibility: public export

index : Nat -> Stream a -> a

  Get the nth element of a stream

Totality: total
Visibility: public export

zipWithIndexLinear : (0 f : (a -> a -> {a:5782})) -> (xs : Stream a) -> (ys : Stream a) -> (i : Nat) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)

Totality: total
Visibility: export

zipWith3IndexLinear : (0 f : (a -> a -> a -> {a:5868})) -> (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
Visibility: export

diag : Stream (Stream a) -> Stream a

  Return the diagonal elements of a stream of streams

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

zig : List1 (Stream a) -> Stream (Stream a) -> Stream a

Totality: total
Visibility: public export

zag : List1 a -> List1 (Stream a) -> Stream (Stream a) -> Stream a

Totality: total
Visibility: public export

cantor : Stream (Stream a) -> Stream a

Totality: total
Visibility: public export

planeWith : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> Stream a -> ((x : a) -> Stream (p x)) -> Stream c

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export

plane : {0 p : a -> Type} -> Stream a -> ((x : a) -> Stream (p x)) -> Stream (x : a ** p x)

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export

planeWith : (a -> b -> c) -> Stream a -> (a -> Stream b) -> Stream c

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export

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

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export