Idris2Doc : Data.Colist

Data.Colist

dataColist : Type -> Type
  A possibly finite Stream.

Totality: total
Constructors:
Nil : Colista
(::) : a -> Inf (Colista) -> Colista
dataInBounds : Nat -> Colista -> 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 : InBounds0 (x::xs)
  Z is a valid index into any cons cell
InLater : InBoundsk Force xs -> InBounds (Sk) (x::xs)
  Valid indices can be extended
append : Colista -> Colista -> Colista
  Concatenate two `Colist`s.

Totality: total
appendl : Colista -> Lista -> Colista
  Append a `List` to a `Colist`.

Totality: total
cycle : Lista -> Colista
  Produce a `Colist` by repeating a sequence.

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

Totality: total
fromList : Lista -> Colista
  Convert a list to a `Colist`.

Totality: total
fromStream : Streama -> Colista
  Convert a stream to a `Colist`.

Totality: total
head : Colista -> Maybea
  Try to extract the first element from a `Colist`.

Totality: total
inBounds : (k : Nat) -> (xs : Colista) -> Dec (InBoundskxs)
  Decide whether `k` is a valid index into Colist `xs`

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

Totality: total
index' : (k : Nat) -> (xs : Colista) -> {auto 0 _ : InBoundskxs} -> a
  Find a particular element of a Colist using InBounds

@ ok a proof that the index is within bounds

Totality: total
isCons : Colista -> Bool
  True, if the given `Colist` is non-empty.

Totality: total
isNil : Colista -> Bool
  True, if this is the empty `Colist`.

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

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

Totality: total
lappend : Lista -> Colista -> Colista
  Append a `Colist` to a `List`.

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

Totality: total
replicate : Nat -> a -> Colista
  Create a `Colist` of `n` replications of the given element.

Totality: total
scanl : (a -> b -> a) -> a -> Colistb -> Colista
  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 -> Colista
  Create a `Colist` of only a single element.

Totality: total
tail : Colista -> Maybe (Colista)
  Try to drop the first element from a `Colist`.
This returns `Nothing` if the given `Colist` is
empty.

Totality: total
take : Nat -> Colista -> Lista
  Take up to `n` elements from a `Colist`.

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

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

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

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

Totality: total
uncons : Colista -> Maybe (a, Colista)
  Try to extract the head and tail of a `Colist`.

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

Totality: total