Idris2Doc : Data.Seq.Unsized

# Data.Seq.Unsized

```General purpose two-end finite sequences.

This is implemented by finger tree.
```

## Reexports

`import public Data.Zippable`

## Definitions

`data Seq : Type -> Type`
`  A two-end finite sequences.`

Totality: total
Visibility: export
Constructor:
`MkSeq : FingerTree (Elem e) -> Seq e`

Hints:
`Applicative Seq`
`Eq a => Eq (Seq a)`
`Foldable Seq`
`Functor Seq`
`Monad Seq`
`Monoid (Seq a)`
`Ord a => Ord (Seq a)`
`Semigroup (Seq a)`
`Show a => Show (Seq a)`
`Sized (Seq a)`
`Traversable Seq`
`Zippable Seq`
`empty : Seq e`
`  O(1). The empty sequence.`

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

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

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

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

Totality: total
Visibility: export
`cons : e -> Seq e -> Seq e`
`  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 : Seq e -> e -> Seq e`
`  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
`(++) : Seq e -> Seq e -> Seq e`
`  O(log(min(m, n))). Concatenate two sequences.`

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

Totality: total
Visibility: export
`head : Seq a -> Maybe a`
`  O(1). The first element of the sequence.`

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

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

Totality: total
Visibility: export
`init : Seq a -> Seq a`
`  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 : Seq a -> Maybe a`
`  O(1). The last element of the sequence.`

Totality: total
Visibility: export
`fromList : List a -> Seq a`
`  O(n). Turn a list into a sequence.`

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

Totality: total
Visibility: export
`adjust : (a -> a) -> Nat -> Seq a -> Seq a`
`  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 -> Seq a -> Seq a`
`  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 -> Seq a -> (Seq a, Seq a)`
`  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 -> Seq a -> Seq a`
`  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 -> Seq a -> Seq a`
`  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' : Show a => Seq a -> String`
`  Dump the internal structure of the finger tree.`

Totality: total
Visibility: export