Idris2Doc : Data.Colist1

Data.Colist1

Colist1 : 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