Data.Colist

Reexports

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

ZippableColist : Zippable Colist

Totality: total
Visibility: public export