Data.RRBVector1.Unsized

Linear Relaxed Radix Balanced Vectors (RRBVector1)

Reexports

Definitions

empty : F1 s (RRBVector1 s a)

  The empty vector. O(1)

Totality: total
Visibility: export

singleton : a -> F1 s (RRBVector1 s a)

  A vector with a single element. O(1)

Totality: total
Visibility: export

fromList : List a -> F1 s (RRBVector1 s a)

  Create a new vector from a list. O(n)

Totality: total
Visibility: export

replicate : Nat -> a -> F1 s (RRBVector1 s a)

  Creates a vector of length n with every element set to x. O(log n)

Totality: total
Visibility: export

toList : RRBVector1 s a -> F1 s (List a)

  Convert a vector to a list. O(n)

Totality: total
Visibility: export

null : RRBVector1 s a -> F1 s Bool

  Is the vector empty? O(1)

Totality: total
Visibility: export

length : RRBVector1 s a -> F1 s Nat

  Return the size of a vector. O(1)

Totality: total
Visibility: export

lookup : Nat -> RRBVector1 s a -> F1 s (Maybe a)

  The element at the index or Nothing if the index is out of range. O(log n)

Totality: total
Visibility: export

index : Nat -> RRBVector1 s a -> F1 s a

  The element at the index.
  Calls 'idris_crash' if the index is out of range. O(log n)

Totality: total
Visibility: export

(!?) : RRBVector1 s a -> Nat -> F1 s (Maybe a)

  A flipped version of lookup. O(log n)

Totality: total
Visibility: export

(!!) : RRBVector1 s a -> Nat -> F1 s a

  A flipped version of index. O(log n)

Totality: total
Visibility: export

update : Nat -> a -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Update the element at the index with a new element.
  If the index is out of range, the original vector is returned. O(log n)

Totality: total
Visibility: export

adjust : Nat -> (a -> a) -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Adjust the element at the index by applying the function to it.
  If the index is out of range, the original vector is returned. O(log n)

Totality: total
Visibility: export

take : Nat -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  The first i elements of the vector.
  If the vector contains less than or equal to i elements, the whole vector is returned. O(log n)

Totality: total
Visibility: export

drop : Nat -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  The vector without the first i elements.
  If the vector contains less than or equal to i elements, the empty vector is returned. O(log n)

Totality: total
Visibility: export

splitAt : Nat -> RRBVector1 s a -> F1 s (RRBVector1 s a, RRBVector1 s a)

  Split the vector at the given index. O(log n)

Totality: total
Visibility: export

viewl : RRBVector1 s a -> F1 s (Maybe (a, RRBVector1 s a))

  The first element and the vector without the first element, or 'Nothing' if the vector is empty. O(log n)

Totality: total
Visibility: export

viewr : RRBVector1 s a -> F1 s (Maybe (RRBVector1 s a, a))

  The vector without the last element and the last element, or 'Nothing' if the vector is empty. O(log n)

Totality: total
Visibility: export

map : (a -> a) -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Apply the function to every element. O(n)

Totality: total
Visibility: export

(<|) : a -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Add an element to the left end of the vector. O(log n)

Totality: total
Visibility: export
Fixity Declarations:
infixr operator, level 0
infixr operator, level 5
infixr operator, level 5

(|>) : RRBVector1 s a -> a -> F1 s (RRBVector1 s a)

  Add an element to the right end of the vector. O(log n)

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 0
infixl operator, level 5
infixl operator, level 5

(><) : RRBVector1 s a -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Concatenates two vectors. O(log(max(n1,n2)))

Totality: total
Visibility: export
Fixity Declarations:
infixr operator, level 5
infixr operator, level 5

insertAt : Nat -> a -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Insert an element at the given index, shifting the rest of the vector over.
  If the index is negative, add the element to the left end of the vector.
  If the index is bigger than or equal to the length of the vector, add the element to the right end of the vector. O(log n)

Totality: total
Visibility: export

deleteAt : Nat -> RRBVector1 s a -> F1 s (RRBVector1 s a)

  Delete the element at the given index.
  If the index is out of range, return the original vector. O(log n)

Totality: total
Visibility: export