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.Fin
import public Data.Nat
import public Data.Vect
import 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)
Sized (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