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
`  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