- data Colist : Type -> Type
A possibly finite Stream.
Totality: total
Constructors:
- Nil : Colist a
- (::) : a -> Inf (Colist a) -> Colist a
- data InBounds : Nat -> Colist a -> Type
Satisfiable if `k` is a valid index into `xs`
@ k the potential index
@ xs the Colist into which k may be an index
Totality: total
Constructors:
- InFirst : InBounds 0 (x :: xs)
Z is a valid index into any cons cell
- InLater : InBounds k Force xs -> InBounds (S k) (x :: xs)
Valid indices can be extended
- append : Colist a -> Colist a -> Colist a
Concatenate two `Colist`s.
Totality: total- appendl : Colist a -> List a -> Colist a
Append a `List` to a `Colist`.
Totality: total- cycle : List a -> Colist a
Produce a `Colist` by repeating a sequence.
Totality: total- drop : Nat -> Colist a -> Colist a
Drop up to `n` elements from the beginning of the `Colist`.
Totality: total- fromList : List a -> Colist a
Convert a list to a `Colist`.
Totality: total- fromStream : Stream a -> Colist a
Convert a stream to a `Colist`.
Totality: total- head : Colist a -> Maybe a
Try to extract the first element from a `Colist`.
Totality: total- inBounds : (k : Nat) -> (xs : Colist a) -> Dec (InBounds k xs)
Decide whether `k` is a valid index into Colist `xs`
Totality: total- index : Nat -> Colist a -> Maybe a
Try to extract the `n`-th element from a `Colist`.
Totality: total- index' : (k : Nat) -> (xs : Colist a) -> {auto 0 _ : InBounds k xs} -> a
Find a particular element of a Colist using InBounds
@ ok a proof that the index is within bounds
Totality: total- isCons : Colist a -> Bool
True, if the given `Colist` is non-empty.
Totality: total- isNil : Colist a -> Bool
True, if this is the empty `Colist`.
Totality: total- iterate : (a -> a) -> a -> Colist a
Generate an infinite `Colist` by repeatedly applying a function.
Totality: total- iterateMaybe : (a -> Maybe a) -> Maybe a -> Colist a
Generate a `Colist` by repeatedly applying a function.
This stops once the function returns `Nothing`.
Totality: total- lappend : List a -> Colist a -> Colist a
Append a `Colist` to a `List`.
Totality: total- repeat : a -> Colist a
An infinite `Colist` of repetitions of the same element.
Totality: total- replicate : Nat -> a -> Colist a
Create a `Colist` of `n` replications of the given element.
Totality: total- scanl : (a -> b -> a) -> a -> Colist b -> Colist a
Produce a `Colist` of left folds of prefixes of the given `Colist`.
@ f the combining function
@ acc the initial value
@ xs the `Colist` to process
Totality: total- singleton : a -> Colist a
Create a `Colist` of only a single element.
Totality: total- tail : Colist a -> Maybe (Colist a)
Try to drop the first element from a `Colist`.
This returns `Nothing` if the given `Colist` is
empty.
Totality: total- take : Nat -> Colist a -> List a
Take up to `n` elements from a `Colist`.
Totality: total- takeBefore : (a -> Bool) -> Colist a -> Colist a
Take elements from a `Colist` up to (but not including) the
first element, for which `p` returns `True`.
Totality: total- takeUntil : (a -> Bool) -> Colist a -> Colist a
Take elements from a `Colist` up to and including the
first element, for which `p` returns `True`.
Totality: total- takeWhile : (a -> Bool) -> Colist a -> Colist a
Take elements from a `Colist` while the given predicate
returns `True`.
Totality: total- takeWhileJust : Colist (Maybe a) -> Colist a
Extract all values wrapped in `Just` from the beginning
of a `Colist`. This stops, once the first `Nothing` is encountered.
Totality: total- uncons : Colist a -> Maybe (a, Colist a)
Try to extract the head and tail of a `Colist`.
Totality: total- unfold : (s -> Maybe (s, a)) -> s -> Colist a
Generate an `Colist` by repeatedly applying a function
to a seed value.
This stops once the function returns `Nothing`.
Totality: total