Idris2Doc : Data.Colist1

Data.Colist1

Reexports

importpublic Data.Zippable

Definitions

dataColist1 : Type->Type
  A possibly finite, non-empty Stream.

Totality: total
Visibility: public export
Constructor: 
(:::) : a->Colista->Colist1a

Hints:
ApplicativeColist1
FunctorColist1
Semigroup (Colist1a)
ZippableColist1
fromList1 : List1a->Colist1a
  Convert a `List1` to a `Colist1`.

Totality: total
Visibility: public export
fromStream : Streama->Colist1a
  Convert a stream to a `Colist1`.

Totality: total
Visibility: public export
fromColist : Colista->Maybe (Colist1a)
  Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
the given `Colist` is empty.

Totality: total
Visibility: public export
fromList : Lista->Maybe (Colist1a)
  Try to convert a list to a `Colist1`. Returns `Nothing` if
the given list is empty.

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

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

Totality: total
Visibility: public export
replicate : (n : Nat) -> {auto0_ : IsSuccn} ->a->Colist1a
  Create a `Colist1` of `n` replications of the given element.

Totality: total
Visibility: public export
cycle : List1a->Colist1a
  Produce a `Colist1` by repeating a sequence

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

Totality: total
Visibility: public export
iterateMaybe : (a->Maybea) ->a->Colist1a
  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->Colist1a
  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 : Colist1a->Colista
  Convert a `Colist1` to a `Colist`

Totality: total
Visibility: public export
forgetInf : Inf (Colist1a) -> Inf (Colista)
  Convert an `Inf (Colist1 a)` to an `Inf (Colist a)`

Totality: total
Visibility: public export
cons : a->Colist1a->Colist1a
  Prepends an element to a `Colist1`.

Totality: total
Visibility: public export
append : Colist1a->Colist1a->Colist1a
  Concatenate two `Colist1`s

Totality: total
Visibility: public export
lappend : Lista->Colist1a->Colist1a
  Append a `Colist1` to a `List`.

Totality: total
Visibility: public export
appendl : Colist1a->Lista->Colist1a
  Append a `List` to a `Colist1`.

Totality: total
Visibility: public export
uncons : Colist1a-> (a, Colista)
  Take a `Colist1` apart

Totality: total
Visibility: public export
head : Colist1a->a
  Extract the first element from a `Colist1`

Totality: total
Visibility: public export
tail : Colist1a->Colista
  Drop the first element from a `Colist1`

Totality: total
Visibility: public export
take : (n : Nat) -> {auto0_ : IsSuccn} ->Colist1a->List1a
  Take up to `n` elements from a `Colist1`

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

Totality: total
Visibility: public export
takeWhileJust : Colist1 (Maybea) ->Colista
  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->Colist1a->Colista
  Drop up to `n` elements from the beginning of the `Colist1`.

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

Totality: total
Visibility: public export
scanl : (a->b->a) ->a->Colist1b->Colist1a
  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 : ZippableColist1
Totality: total
Visibility: public export
zig : List1 (Colist1a) ->Colist (Colist1a) ->Colista
Totality: total
Visibility: public export
zag : List1a->List (Colist1a) ->Colist (Colist1a) ->Colista
Totality: total
Visibility: public export
cantor : Colist1 (Colist1a) ->Colist1a
Totality: total
Visibility: public export
cantor : List (Colista) ->Colista
Totality: total
Visibility: public export
planeWith : {0p : a->Type} -> ((x : a) ->px->c) ->Colist1a-> ((x : a) ->Colist1 (px)) ->Colist1c
  Explore the plane corresponding to all possible pairings
using Cantor's zig zag traversal

Totality: total
Visibility: public export
plane : {0p : a->Type} ->Colist1a-> ((x : a) ->Colist1 (px)) ->Colist1 (x : a**px)
  Explore the plane corresponding to all possible pairings
using Cantor's zig zag traversal

Totality: total
Visibility: public export
planeWith : (a->b->c) ->Colist1a-> (a->Colist1b) ->Colist1c
  Explore the plane corresponding to all possible pairings
using Cantor's zig zag traversal

Totality: total
Visibility: public export
plane : Colist1a-> (a->Colist1b) ->Colist1 (a, b)
  Explore the plane corresponding to all possible pairings
using Cantor's zig zag traversal

Totality: total
Visibility: public export