General purpose two-end finite sequences. This is implemented by finger tree.

`import public Data.Zippable`

`data Seq : Type -> Type`

A two-end finite sequences.

**Totality**: total

**Visibility**: export

**Constructor**:`MkSeq : FingerTree (Elem e) -> Seq e`

**Hints**:`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