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: exportsingleton : e -> Seq e
O(1). A singleton sequence.
Totality: total
Visibility: exportreplicate : Nat -> e -> Seq e
O(n). A sequence of length n with a the value of every element.
Totality: total
Visibility: exportlength : Seq a -> Nat
O(1). The number of elements in the sequence.
Totality: total
Visibility: exportreverse : Seq a -> Seq a
O(n). Reverse the sequence.
Totality: total
Visibility: exportcons : 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 5snoc : 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 7viewl : Seq a -> Maybe (a, Seq a)
O(1). View from the left of the sequence.
Totality: total
Visibility: exporthead : Seq a -> Maybe a
O(1). The first element of the sequence.
Totality: total
Visibility: exporttail : 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: exportviewr : Seq a -> Maybe (Seq a, a)
O(1). View from the right of the sequence.
Totality: total
Visibility: exportinit : 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: exportlast : Seq a -> Maybe a
O(1). The last element of the sequence.
Totality: total
Visibility: exportfromList : List a -> Seq a
O(n). Turn a list into a sequence.
Totality: total
Visibility: exportindex : Nat -> Seq a -> Maybe a
O(log(min(i, n-i))). The element at the specified position.
Totality: total
Visibility: exportadjust : (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: exportupdate : 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: exportsplitAt : 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: exporttake : 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: exportdrop : 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: exportshow' : Show a => Seq a -> String
Dump the internal structure of the finger tree.
Totality: total
Visibility: export