- data Colist1 : Type -> Type
A possibly finite, non-empty Stream.
Totality: total
Constructor: - (:::) : a -> Colist a -> Colist1 a
- append : Colist1 a -> Colist1 a -> Colist1 a
Concatenate two `Colist1`s
Totality: total- appendl : Colist1 a -> List a -> Colist1 a
Append a `List` to a `Colist1`.
Totality: total- cantor : Colist1 (Colist1 a) -> Colist1 a
- Totality: total
- cons : a -> Colist1 a -> Colist1 a
Prepends an element to a `Colist1`.
Totality: total- cycle : List1 a -> Colist1 a
Produce a `Colist1` by repeating a sequence
Totality: total- drop : Nat -> Colist1 a -> Colist a
Drop up to `n` elements from the beginning of the `Colist1`.
Totality: total- forget : Colist1 a -> Colist a
Convert a `Colist1` to a `Colist`
Totality: total- forgetInf : Inf (Colist1 a) -> Inf (Colist a)
Convert an `Inf (Colist1 a)` to an `Inf (Colist a)`
Totality: total- fromColist : Colist a -> Maybe (Colist1 a)
Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
the given `Colist` is empty.
Totality: total- fromList : List a -> Maybe (Colist1 a)
Try to convert a list to a `Colist1`. Returns `Nothing` if
the given list is empty.
Totality: total- fromList1 : List1 a -> Colist1 a
Convert a `List1` to a `Colist1`.
Totality: total- fromStream : Stream a -> Colist1 a
Convert a stream to a `Colist1`.
Totality: total- head : Colist1 a -> a
Extract the first element from a `Colist1`
Totality: total- index : Nat -> Colist1 a -> Maybe a
Try to extract the `n`-th element from a `Colist1`.
Totality: total- iterate : (a -> a) -> a -> Colist1 a
Generate an infinite `Colist1` by repeatedly applying a function.
Totality: total- iterateMaybe : (a -> Maybe a) -> a -> Colist1 a
Generate a `Colist1` by repeatedly applying a function.
This stops once the function returns `Nothing`.
Totality: total- lappend : List a -> Colist1 a -> Colist1 a
Append a `Colist1` to a `List`.
Totality: total- repeat : a -> Colist1 a
An infinite `Colist1` of repetitions of the same element.
Totality: total- replicate : (n : Nat) -> {auto 0 _ : IsSucc n} -> a -> Colist1 a
Create a `Colist1` of `n` replications of the given element.
Totality: total- scanl : (a -> b -> a) -> a -> Colist1 b -> Colist1 a
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 -> Colist1 a
Create a `Colist1` of only a single element.
Totality: total- tail : Colist1 a -> Colist a
Drop the first element from a `Colist1`
Totality: total- take : (n : Nat) -> {auto 0 _ : IsSucc n} -> Colist1 a -> List1 a
Take up to `n` elements from a `Colist1`
Totality: total- takeBefore : (a -> Bool) -> Colist1 a -> Colist a
Take elements from a `Colist1` up to (but not including) the
first element, for which `p` returns `True`.
Totality: total- takeUntil : (a -> Bool) -> Colist1 a -> Colist1 a
Take elements from a `Colist1` up to and including the
first element, for which `p` returns `True`.
Totality: total- takeWhile : (a -> Bool) -> Colist1 a -> Colist a
Take elements from a `Colist1` while the given predicate `p`
returns `True`.
Totality: total- takeWhileJust : Colist1 (Maybe a) -> Colist a
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 -> Colist1 a
Generate a `Colist1` by repeatedly applying a function
to a seed value.
This stops once the function returns `Nothing`.
Totality: total- zag : List1 a -> List1 (Colist a) -> Colist (Colist1 a) -> Colist1 a
- Totality: total
- zig : List1 (Colist1 a) -> Colist (Colist1 a) -> Colist1 a
- Totality: total