Idris2Doc : Data.Seq.Sized

# Data.Seq.Sized

```General purpose two-end finite sequences,
with length in its type.

This is implemented by finger tree.
```

## Reexports

`import public Data.Finimport public Data.Natimport public Data.Vectimport public Data.Zippable`

## Definitions

`data Seq : Nat -> Type -> Type`
`  A two-end finite sequences, with length in its type.`

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

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

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

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

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

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

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

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

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

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

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

Totality: total
Visibility: export
`tail : Seq (S n) a -> Seq n a`
`  O(1). The elements after the head of the sequence.`

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

Totality: total
Visibility: export
`init : Seq (S n) a -> Seq n a`
`  O(1). The elements before the last element of the sequence.`

Totality: total
Visibility: export
`last : Seq (S n) a -> a`
`  O(1). The last element of the sequence.`

Totality: total
Visibility: export
`fromVect : Vect n a -> Seq n a`
`  O(n). Turn a vector into a sequence.`

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

Totality: total
Visibility: export
`toVect : Seq n a -> Vect n a`
`  O(n). Turn a sequence into a vector.`

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

Totality: total
Visibility: export
`index' : Seq n a -> Fin n -> a`
`  O(log(min(i, n-i))). The element at the specified position.  Use Fin n to index instead.`

Totality: total
Visibility: export
`adjust : (a -> a) -> (i : Nat) -> Seq n a -> LT i n => Seq n a`
`  O(log(min(i, n-i))). Update the element at the specified position.`

Totality: total
Visibility: export
`update : (i : Nat) -> a -> Seq n a -> LT i n => Seq n a`
`  O(log(min(i, n-i))). Replace the element at the specified position.`

Totality: total
Visibility: export
`splitAt : (i : Nat) -> Seq (i + j) a -> (Seq i a, Seq j a)`
`  O(log(min(i, n-i))). Split a sequence at a given position.`

Totality: total
Visibility: export
`take : (i : Nat) -> Seq (i + j) a -> Seq i a`
`  O(log(min(i, n-i))). The first i elements of a sequence.`

Totality: total
Visibility: export
`drop : (i : Nat) -> Seq (i + j) a -> Seq j a`
`  O(log(min(i, n-i))). Elements of a sequence after the first i.`

Totality: total
Visibility: export
`show' : Show a => Seq n a -> String`
`  Dump the internal structure of the finger tree.`

Totality: total
Visibility: export