Idris2Doc : Data.Colist

# Data.Colist

## Reexports

`import public Data.Zippable`

## Definitions

`data Colist : Type -> Type`
`  A possibly finite Stream.`

Totality: total
Visibility: public export
Constructors:
`Nil : Colist a`
`(::) : a -> Inf (Colist a) -> Colist a`

Hints:
`Applicative Colist`
`Functor Colist`
`Monoid (Colist a)`
`Semigroup (Colist a)`
`Uninhabited (InBounds k xs) => Uninhabited (InBounds (S k) (x :: Delay xs))`
`Zippable Colist`
`fromList : List a -> Colist a`
`  Convert a list to a `Colist`.`

Totality: total
Visibility: public export
`fromStream : Stream a -> Colist a`
`  Convert a stream to a `Colist`.`

Totality: total
Visibility: public export
`singleton : a -> Colist a`
`  Create a `Colist` of only a single element.`

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

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

Totality: total
Visibility: public export
`cycle : List a -> Colist a`
`  Produce a `Colist` by repeating a sequence.`

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

Totality: total
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`isNil : Colist a -> Bool`
`  True, if this is the empty `Colist`.`

Totality: total
Visibility: public export
`isCons : Colist a -> Bool`
`  True, if the given `Colist` is non-empty.`

Totality: total
Visibility: public export
`append : Colist a -> Colist a -> Colist a`
`  Concatenate two `Colist`s.`

Totality: total
Visibility: public export
`lappend : List a -> Colist a -> Colist a`
`  Append a `Colist` to a `List`.`

Totality: total
Visibility: public export
`appendl : Colist a -> List a -> Colist a`
`  Append a `List` to a `Colist`.`

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

Totality: total
Visibility: public export
`head : Colist a -> Maybe a`
`  Try to extract the first element from a `Colist`.`

Totality: total
Visibility: public export
`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
Visibility: public export
`take : Nat -> Colist a -> List a`
`  Take up to `n` elements from a `Colist`.`

Totality: total
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
`takeWhile : (a -> Bool) -> Colist a -> Colist a`
`  Take elements from a `Colist` while the given predicate  returns `True`.`

Totality: total
Visibility: public export
`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
Visibility: public export
`drop : Nat -> Colist a -> Colist a`
`  Drop up to `n` elements from the beginning of the `Colist`.`

Totality: total
Visibility: public export
`index : Nat -> Colist a -> Maybe a`
`  Try to extract the `n`-th element from a `Colist`.`

Totality: total
Visibility: public export
`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
Visibility: public export
`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
Visibility: public export
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`

Hints:
`Uninhabited (InBounds k [])`
`Uninhabited (InBounds k xs) => Uninhabited (InBounds (S k) (x :: Delay xs))`
`inBounds : (k : Nat) -> (xs : Colist a) -> Dec (InBounds k xs)`
`  Decide whether `k` is a valid index into Colist `xs``

Totality: total
Visibility: public export
`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
Visibility: public export