Data.Colist1

Reexports

import public Data.Zippable

Definitions

data Colist1 : Type -> Type

  A possibly finite, non-empty Stream.

Totality: total
Visibility: public export
Constructor:

(:::) : a -> Colist a -> Colist1 a

Hints:

Applicative Colist1
Functor Colist1
Semigroup (Colist1 a)
Zippable Colist1

fromList1 : List1 a -> Colist1 a

  Convert a `List1` to a `Colist1`.

Totality: total
Visibility: public export

fromStream : Stream a -> Colist1 a

  Convert a stream to a `Colist1`.

Totality: total
Visibility: public export

fromColist : Colist a -> Maybe (Colist1 a)

  Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
  the given `Colist` is empty.

Totality: total
Visibility: public export

fromList : List a -> Maybe (Colist1 a)

  Try to convert a list to a `Colist1`. Returns `Nothing` if
  the given list is empty.

Totality: total
Visibility: public export

singleton : a -> Colist1 a

  Create a `Colist1` of only a single element.

Totality: total
Visibility: public export

repeat : a -> Colist1 a

  An infinite `Colist1` of repetitions of the same element.

Totality: total
Visibility: public export

replicate : (n : Nat) -> {auto 0 _ : IsSucc n} -> a -> Colist1 a

  Create a `Colist1` of `n` replications of the given element.

Totality: total
Visibility: public export

cycle : List1 a -> Colist1 a

  Produce a `Colist1` by repeating a sequence

Totality: total
Visibility: public export

iterate : (a -> a) -> a -> Colist1 a

  Generate an infinite `Colist1` by repeatedly applying a function.

Totality: total
Visibility: public export

iterateMaybe : (a -> Maybe a) -> a -> Colist1 a

  Generate a `Colist1` by repeatedly applying a function.
  This stops once the function returns `Nothing`.

Totality: total
Visibility: public export

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

forget : Colist1 a -> Colist a

  Convert a `Colist1` to a `Colist`

Totality: total
Visibility: public export

forgetInf : Inf (Colist1 a) -> Inf (Colist a)

  Convert an `Inf (Colist1 a)` to an `Inf (Colist a)`

Totality: total
Visibility: public export

cons : a -> Colist1 a -> Colist1 a

  Prepends an element to a `Colist1`.

Totality: total
Visibility: public export

append : Colist1 a -> Colist1 a -> Colist1 a

  Concatenate two `Colist1`s

Totality: total
Visibility: public export

lappend : List a -> Colist1 a -> Colist1 a

  Append a `Colist1` to a `List`.

Totality: total
Visibility: public export

appendl : Colist1 a -> List a -> Colist1 a

  Append a `List` to a `Colist1`.

Totality: total
Visibility: public export

uncons : Colist1 a -> (a, Colist a)

  Take a `Colist1` apart

Totality: total
Visibility: public export

head : Colist1 a -> a

  Extract the first element from a `Colist1`

Totality: total
Visibility: public export

tail : Colist1 a -> Colist a

  Drop the first element from a `Colist1`

Totality: total
Visibility: public export

take : (n : Nat) -> {auto 0 _ : IsSucc n} -> Colist1 a -> List1 a

  Take up to `n` elements from a `Colist1`

Totality: total
Visibility: public export

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

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

takeWhile : (a -> Bool) -> Colist1 a -> Colist a

  Take elements from a `Colist1` while the given predicate `p`
  returns `True`.

Totality: total
Visibility: public export

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

drop : Nat -> Colist1 a -> Colist a

  Drop up to `n` elements from the beginning of the `Colist1`.

Totality: total
Visibility: public export

index : Nat -> Colist1 a -> Maybe a

  Try to extract the `n`-th element from a `Colist1`.

Totality: total
Visibility: public export

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
Visibility: export

ZippableColist1 : Zippable Colist1

Totality: total
Visibility: public export

zig : List1 (Colist1 a) -> Colist (Colist1 a) -> Colist a

Totality: total
Visibility: public export

zag : List1 a -> List (Colist1 a) -> Colist (Colist1 a) -> Colist a

Totality: total
Visibility: public export

cantor : Colist1 (Colist1 a) -> Colist1 a

Totality: total
Visibility: public export

cantor : List (Colist a) -> Colist a

Totality: total
Visibility: public export

planeWith : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> Colist1 a -> ((x : a) -> Colist1 (p x)) -> Colist1 c

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export

plane : {0 p : a -> Type} -> Colist1 a -> ((x : a) -> Colist1 (p x)) -> Colist1 (x : a ** p x)

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export

planeWith : (a -> b -> c) -> Colist1 a -> (a -> Colist1 b) -> Colist1 c

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export

plane : Colist1 a -> (a -> Colist1 b) -> Colist1 (a, b)

  Explore the plane corresponding to all possible pairings
  using Cantor's zig zag traversal

Totality: total
Visibility: public export