Data.Vector

v11.3.15 • Indexed Vectors

Length-indexed vectors, providing static guarantees about the number of elements.

Types

Vector :: * -> Nat -> *

A vector of elements of type A with length n.

Implementation 
data Vector A (n : Nat) = Nil | Cons A (Vector A n)

Functions

head :: Vector A n -> Maybe A

Safely retrieve the head of a list.

Implementation 
hd xs = case xs of
    Nil      -> Nothing
    Cons h t -> Just h

length :: Vector A n -> Nat

Returns the length of the vector.

Implementation 
length v = case v of
    Nil -> Zero
    Cons h t -> Succ t