IdrisDoc: Data.BoundedList

# Data.BoundedList

zeroBoundIsEmpty : (xs : BoundedList (fromInteger 0) a) -> xs = the (BoundedList (fromInteger 0) a) []
weaken : BoundedList n a -> BoundedList (n + m) a

  Loosen the bounds on a list's length.

toVect : (xs : BoundedList n a) -> Vect (finToNat (length xs)) a

  Convert bounded list to vector.

toList : BoundedList n a -> List a
take : (n : Nat) -> List a -> BoundedList n a
replicate : (n : Nat) -> a -> BoundedList n a
pad : BoundedList n a -> a -> BoundedList n a

  Extend a bounded list to the maximum size by padding on the left.

length : BoundedList n a -> Fin (S n)

  Compute the length of a list.

index : Fin (S n) -> BoundedList n a -> Maybe a
fromVect : (xs : Vect n a) -> BoundedList n a

  Convert vector to bounded list.

fromList : (xs : List a) -> BoundedList (length xs) a
data BoundedList : Nat -> Type -> Type

  A list with an upper bound on its length.

  Nil : BoundedList n a
  (::) : a -> BoundedList n a -> BoundedList (S n) a
    Fixity
      Left associative, precedence 7