Idris2Doc : Data.Seq.Unsized

Data.Seq.Unsized

General purpose two-end finite sequences.

This is implemented by finger tree.

Reexports

importpublic Data.Zippable

Definitions

dataSeq : Type->Type
  A two-end finite sequences.

Totality: total
Visibility: export
Constructor: 
MkSeq : FingerTree (Eleme) ->Seqe

Hints:
ApplicativeSeq
Eqa=>Eq (Seqa)
FoldableSeq
FunctorSeq
MonadSeq
Monoid (Seqa)
Orda=>Ord (Seqa)
Semigroup (Seqa)
Showa=>Show (Seqa)
Sized (Seqa)
TraversableSeq
ZippableSeq
empty : Seqe
  O(1). The empty sequence.

Totality: total
Visibility: export
singleton : e->Seqe
  O(1). A singleton sequence.

Totality: total
Visibility: export
replicate : Nat->e->Seqe
  O(n). A sequence of length n with a the value of every element.

Totality: total
Visibility: export
length : Seqa->Nat
  O(1). The number of elements in the sequence.

Totality: total
Visibility: export
reverse : Seqa->Seqa
  O(n). Reverse the sequence.

Totality: total
Visibility: export
cons : e->Seqe->Seqe
  O(1). Add an element to the left end of a sequence.

Totality: total
Visibility: export
Fixity Declarations:
infixr operator, level 5
infixr operator, level 5
snoc : Seqe->e->Seqe
  O(1). Add an element to the right end of a sequence.

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 5
infixl operator, level 5
(++) : Seqe->Seqe->Seqe
  O(log(min(m, n))). Concatenate two sequences.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7
viewl : Seqa->Maybe (a, Seqa)
  O(1). View from the left of the sequence.

Totality: total
Visibility: export
head : Seqa->Maybea
  O(1). The first element of the sequence.

Totality: total
Visibility: export
tail : Seqa->Seqa
  O(1). The elements after the head of the sequence.
Returns an empty sequence when the sequence is empty.

Totality: total
Visibility: export
viewr : Seqa->Maybe (Seqa, a)
  O(1). View from the right of the sequence.

Totality: total
Visibility: export
init : Seqa->Seqa
  O(1). The elements before the last element of the sequence.
Returns an empty sequence when the sequence is empty.

Totality: total
Visibility: export
last : Seqa->Maybea
  O(1). The last element of the sequence.

Totality: total
Visibility: export
fromList : Lista->Seqa
  O(n). Turn a list into a sequence.

Totality: total
Visibility: export
index : Nat->Seqa->Maybea
  O(log(min(i, n-i))). The element at the specified position.

Totality: total
Visibility: export
adjust : (a->a) ->Nat->Seqa->Seqa
  O(log(min(i, n-i))). Update the element at the specified position.
If the position is out of range, the original sequence is returned.

Totality: total
Visibility: export
update : Nat->a->Seqa->Seqa
  O(log(min(i, n-i))). Replace the element at the specified position.
If the position is out of range, the original sequence is returned.

Totality: total
Visibility: export
splitAt : Nat->Seqa-> (Seqa, Seqa)
  O(log(min(i, n-i))). Split a sequence at a given position.
splitAt i s = (take i s, drop i s)

Totality: total
Visibility: export
take : Nat->Seqa->Seqa
  O(log(min(i,n-i))). The first i elements of a sequence.
If the sequence contains fewer than i elements, the whole sequence is returned.

Totality: total
Visibility: export
drop : Nat->Seqa->Seqa
  O(log(min(i,n-i))). Elements of a sequence after the first i.
If the sequence contains fewer than i elements, the empty sequence is returned.

Totality: total
Visibility: export
show' : Showa=>Seqa->String
  Dump the internal structure of the finger tree.

Totality: total
Visibility: export