Idris2Doc : Data.Colist1

Data.Colist1

dataColist1 : Type -> Type
  A possibly finite, non-empty Stream.

Totality: total
Constructor: 
(:::) : a -> Colista -> Colist1a
append : Colist1a -> Colist1a -> Colist1a
  Concatenate two `Colist1`s

Totality: total
appendl : Colist1a -> Lista -> Colist1a
  Append a `List` to a `Colist1`.

Totality: total
cantor : Colist1 (Colist1a) -> Colist1a
Totality: total
cons : a -> Colist1a -> Colist1a
  Prepends an element to a `Colist1`.

Totality: total
cycle : List1a -> Colist1a
  Produce a `Colist1` by repeating a sequence

Totality: total
drop : Nat -> Colist1a -> Colista
  Drop up to `n` elements from the beginning of the `Colist1`.

Totality: total
forget : Colist1a -> Colista
  Convert a `Colist1` to a `Colist`

Totality: total
forgetInf : Inf (Colist1a) -> Inf (Colista)
  Convert an `Inf (Colist1 a)` to an `Inf (Colist a)`

Totality: total
fromColist : Colista -> Maybe (Colist1a)
  Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
the given `Colist` is empty.

Totality: total
fromList : Lista -> Maybe (Colist1a)
  Try to convert a list to a `Colist1`. Returns `Nothing` if
the given list is empty.

Totality: total
fromList1 : List1a -> Colist1a
  Convert a `List1` to a `Colist1`.

Totality: total
fromStream : Streama -> Colist1a
  Convert a stream to a `Colist1`.

Totality: total
head : Colist1a -> a
  Extract the first element from a `Colist1`

Totality: total
index : Nat -> Colist1a -> Maybea
  Try to extract the `n`-th element from a `Colist1`.

Totality: total
iterate : (a -> a) -> a -> Colist1a
  Generate an infinite `Colist1` by repeatedly applying a function.

Totality: total
iterateMaybe : (a -> Maybea) -> a -> Colist1a
  Generate a `Colist1` by repeatedly applying a function.
This stops once the function returns `Nothing`.

Totality: total
lappend : Lista -> Colist1a -> Colist1a
  Append a `Colist1` to a `List`.

Totality: total
repeat : a -> Colist1a
  An infinite `Colist1` of repetitions of the same element.

Totality: total
replicate : (n : Nat) -> {auto 0 _ : IsSuccn} -> a -> Colist1a
  Create a `Colist1` of `n` replications of the given element.

Totality: total
scanl : (a -> b -> a) -> a -> Colist1b -> Colist1a
  Produce a `Colist1` of left folds of prefixes of the given `Colist1`.
@ f the combining function
@ acc the initial value
@ xs the `Colist1` to process

Totality: total
singleton : a -> Colist1a
  Create a `Colist1` of only a single element.

Totality: total
tail : Colist1a -> Colista
  Drop the first element from a `Colist1`

Totality: total
take : (n : Nat) -> {auto 0 _ : IsSuccn} -> Colist1a -> List1a
  Take up to `n` elements from a `Colist1`

Totality: total
takeBefore : (a -> Bool) -> Colist1a -> Colista
  Take elements from a `Colist1` up to (but not including) the
first element, for which `p` returns `True`.

Totality: total
takeUntil : (a -> Bool) -> Colist1a -> Colist1a
  Take elements from a `Colist1` up to and including the
first element, for which `p` returns `True`.

Totality: total
takeWhile : (a -> Bool) -> Colist1a -> Colista
  Take elements from a `Colist1` while the given predicate `p`
returns `True`.

Totality: total
takeWhileJust : Colist1 (Maybea) -> Colista
  Extract all values wrapped in `Just` from the beginning
of a `Colist1`. This stops, once the first `Nothing` is encountered.

Totality: total
unfold : (s -> Maybe (s, a)) -> s -> a -> Colist1a
  Generate a `Colist1` by repeatedly applying a function
to a seed value.
This stops once the function returns `Nothing`.

Totality: total
zag : List1a -> List1 (Colista) -> Colist (Colist1a) -> Colist1a
Totality: total
zig : List1 (Colist1a) -> Colist (Colist1a) -> Colist1a
Totality: total