Safe Haskell	None
Language	Haskell2010

Vector

Contents

Synopsis

data Vector (a :: Nat) (b :: TYPE R) where
- Vector :: forall (a :: Nat) (b :: TYPE R). Vector# a b -> Vector a b
data Vector# (a :: Nat) (b :: TYPE R) :: UnliftedType
data MutableVector a (b :: Nat) (c :: TYPE R) where
- MutableVector :: forall a (b :: Nat) (c :: TYPE R). MutableVector# a b c -> MutableVector a b c
data MutableVector# a (b :: Nat) (c :: TYPE R) :: UnliftedType
data Bounded (a :: Nat) (b :: TYPE R) where
- Bounded :: forall (b :: TYPE R) (a :: Nat) (m :: Nat). Nat# m -> (m <=# a) -> Vector# m b -> Bounded a b
data Vector_ (a :: TYPE R) where
- Vector_ :: forall (a :: TYPE R) (n :: Nat). Nat# n -> Vector# n a -> Vector_ a
type family FromMutability# (m :: Mutability) :: Nat -> TYPE R -> UnliftedType where ...
vector_ :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector_ a
write# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> a -> State# s -> State# s
write :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Fin# n -> a -> ST s ()
read# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> State# s -> (# State# s, a #)
index# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> Fin# n -> a
index :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Fin# n -> a
unlift :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Vector# n a
substitute :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector m a -> Vector n a
substitute# :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector# m a -> Vector# n a
initialized :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> ST s (MutableVector s n a)
initialized# :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> State# s -> (# State# s, MutableVector# s n a #)
empty# :: forall (a :: TYPE R). (# #) -> Vector# 0 a
empty :: forall (a :: TYPE R). Vector 0 a
unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat n -> Vector m a -> Vector n a
unsafeCoerceVector :: forall (a :: TYPE R) (b :: TYPE R) (n :: Nat). Vector n a -> Vector n b
unsafeConstruct# :: forall (a :: TYPE R) (n :: Nat). A# a -> Vector# n a
expose :: forall (n :: Nat) (a :: TYPE R). Vector n a -> A# a
expose# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> A# a
freezeSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s (Vector n a)
freezeSlice# :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector# s m a -> Nat# i -> Nat# n -> State# s -> (# State# s, Vector# n a #)
set :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Nat# n -> a -> ST s ()
setSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s n a -> Nat# i -> Nat# m -> a -> ST s ()
unsafeShrinkFreeze :: forall s (n0 :: Nat) (n1 :: Nat) (a :: TYPE R). (n1 <=# n0) -> MutableVector s n0 a -> Nat# n1 -> ST s (Vector n1 a)
unsafeFreeze :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> ST s (Vector n a)
freeze :: forall (n :: Nat) s (a :: TYPE R). Nat# n -> MutableVector s n a -> ST s (Vector n a)
freeze# :: forall (n :: Nat) s (a :: TYPE R). Nat# n -> MutableVector# s n a -> State# s -> (# State# s, Vector# n a #)
thaw :: forall (n :: Nat) (a :: TYPE R) s. Nat# n -> Vector n a -> ST s (MutableVector s n a)
thawSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R) s. ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> ST s (MutableVector s n a)
tail :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector (n + 1) a -> Vector n a
cons :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a
snoc :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a
replaceAt :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Fin# n -> a -> Vector n a
empty_ :: forall (a :: TYPE R). Vector_ a
map :: forall (a :: TYPE R) (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a
all :: forall (a :: TYPE R) (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool
any :: forall (a :: TYPE R) (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool
findIndex :: forall (n :: Nat) (a :: TYPE R). (a -> Bool) -> Nat# n -> Vector n a -> MaybeFin# n
traverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (a -> m b) -> Nat# n -> Vector n a -> m ()
traverseZip_ :: forall (n :: Nat) m (a :: TYPE R) (b :: TYPE R) c. Monad m => (a -> b -> m c) -> Nat# n -> Vector n a -> Vector n b -> m ()
traverseST# :: forall (n :: Nat) s (a :: TYPE R) (b :: TYPE R). (a -> State# s -> (# State# s, b #)) -> Nat# n -> Vector# n a -> State# s -> (# State# s, Vector# n b #)
itraverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector n a -> m ()
itraverse_# :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector# n a -> m ()
foldlM :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (b -> a -> m b) -> b -> Nat# n -> Vector n a -> m b
foldrZip :: forall (n :: Nat) (a :: TYPE R) (b :: TYPE R) c. (a -> b -> c -> c) -> c -> Nat# n -> Vector n a -> Vector n b -> c
foldr :: forall (n :: Nat) (a :: TYPE R) b. (a -> b -> b) -> b -> Nat# n -> Vector n a -> b
ifoldr :: forall (n :: Nat) (a :: TYPE R) b. (Fin# n -> a -> b -> b) -> b -> Nat# n -> Vector n a -> b
ifoldl' :: forall (n :: Nat) (a :: TYPE R) b. (b -> Fin# n -> a -> b) -> b -> Nat# n -> Vector n a -> b
ifoldlSlice' :: forall (i :: Nat) (m :: Nat) (n :: Nat) (a :: TYPE R) b. ((i + n) <= m) -> (b -> Fin# (i + n) -> a -> b) -> b -> Vector m a -> Nat# i -> Nat# n -> b
liftShows :: forall (n :: Nat) (a :: TYPE R). (a -> String -> String) -> Nat# n -> Vector n a -> String -> String
replicate :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a
construct1 :: forall (a :: TYPE R). a -> Vector 1 a
construct2 :: forall (a :: TYPE R). a -> a -> Vector 2 a
construct3 :: forall (a :: TYPE R). a -> a -> a -> Vector 3 a
construct4 :: forall (a :: TYPE R). a -> a -> a -> a -> Vector 4 a
construct5 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> Vector 5 a
construct6 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> Vector 6 a
construct7 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector 7 a
construct1# :: forall (a :: TYPE R). a -> Vector# 1 a
construct2# :: forall (a :: TYPE R). a -> a -> Vector# 2 a
construct3# :: forall (a :: TYPE R). a -> a -> a -> Vector# 3 a
construct4# :: forall (a :: TYPE R). a -> a -> a -> a -> Vector# 4 a
construct7# :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector# 7 a
construct1_ :: forall (a :: TYPE R). a -> Vector_ a
construct2_ :: forall (a :: TYPE R). a -> a -> Vector_ a
construct3_ :: forall (a :: TYPE R). a -> a -> a -> Vector_ a
construct4_ :: forall (a :: TYPE R). a -> a -> a -> a -> Vector_ a
construct7_ :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector_ a
append :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat# n -> Nat# m -> Vector n a -> Vector m a -> Vector (n + m) a
clone :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a
cloneSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R). ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a
copySlice :: forall (di :: Natural) (n :: Natural) (dn :: Nat) (si :: Natural) (sn :: Nat) s (a :: TYPE R). ((di + n) <=# dn) -> ((si + n) <=# sn) -> MutableVector s dn a -> Nat# di -> Vector sn a -> Nat# si -> Nat# n -> ST s ()
index0 :: forall (n :: Natural) (a :: TYPE R). CmpNat 0 n ~ 'LT => Vector n a -> a
index1 :: forall (n :: Natural) (a :: TYPE R). CmpNat 1 n ~ 'LT => Vector n a -> a
index2 :: forall (n :: Natural) (a :: TYPE R). CmpNat 2 n ~ 'LT => Vector n a -> a
index3 :: forall (n :: Natural) (a :: TYPE R). CmpNat 3 n ~ 'LT => Vector n a -> a
index4 :: forall (n :: Natural) (a :: TYPE R). CmpNat 4 n ~ 'LT => Vector n a -> a
index5 :: forall (n :: Natural) (a :: TYPE R). CmpNat 5 n ~ 'LT => Vector n a -> a
index6 :: forall (n :: Natural) (a :: TYPE R). CmpNat 6 n ~ 'LT => Vector n a -> a
index7 :: forall (n :: Natural) (a :: TYPE R). CmpNat 7 n ~ 'LT => Vector n a -> a
index8 :: forall (n :: Natural) (a :: TYPE R). CmpNat 8 n ~ 'LT => Vector n a -> a

Documentation

data Vector (a :: Nat) (b :: TYPE R) where Source #

Constructors

Vector :: forall (a :: Nat) (b :: TYPE R). Vector# a b -> Vector a b

data Vector# (a :: Nat) (b :: TYPE R) :: UnliftedType Source #

data MutableVector a (b :: Nat) (c :: TYPE R) where Source #

Constructors

MutableVector :: forall a (b :: Nat) (c :: TYPE R). MutableVector# a b c -> MutableVector a b c

data MutableVector# a (b :: Nat) (c :: TYPE R) :: UnliftedType Source #

data Bounded (a :: Nat) (b :: TYPE R) where Source #

A vector with a known upper bound on its length but whose exact length is not known.

Constructors

Bounded :: forall (b :: TYPE R) (a :: Nat) (m :: Nat). Nat# m -> (m <=# a) -> Vector# m b -> Bounded a b

data Vector_ (a :: TYPE R) where Source #

A vector in which the length is hidden.

Constructors

Vector_ :: forall (a :: TYPE R) (n :: Nat). Nat# n -> Vector# n a -> Vector_ a

type family FromMutability# (m :: Mutability) :: Nat -> TYPE R -> UnliftedType where ... Source #

A type family that helps the user define data types that support both mutable and immutable vectors.

Equations

FromMutability# 'Immutable = Vector#
FromMutability# ('Mutable s) = MutableVector# s

vector_ :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector_ a Source #

Primitives

write# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> a -> State# s -> State# s Source #

write :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> Fin# n -> a -> ST s () Source #

read# :: forall s (n :: Nat) (a :: TYPE R). MutableVector# s n a -> Fin# n -> State# s -> (# State# s, a #) Source #

index# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> Fin# n -> a Source #

index :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Fin# n -> a Source #

unlift :: forall (n :: Nat) (a :: TYPE R). Vector n a -> Vector# n a Source #

substitute :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector m a -> Vector n a Source #

substitute# :: forall (m :: Nat) (n :: Nat) (a :: TYPE R). (m :=:# n) -> Vector# m a -> Vector# n a Source #

initialized :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> ST s (MutableVector s n a) Source #

initialized# :: forall s (n :: Nat) (a :: TYPE R). Nat# n -> a -> State# s -> (# State# s, MutableVector# s n a #) Source #

empty# :: forall (a :: TYPE R). (# #) -> Vector# 0 a Source #

empty :: forall (a :: TYPE R). Vector 0 a Source #

unsafeCoerceLength :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat n -> Vector m a -> Vector n a Source #

Tell the type system that a vector has a certain length without proving it.

unsafeCoerceVector :: forall (a :: TYPE R) (b :: TYPE R) (n :: Nat). Vector n a -> Vector n b Source #

Unsafely coerce between two vectors of elements that have same runtime representation. For boxed types, this is a bad idea. However, we occassionally need this in order to write functions that validate that all elements satisfy a condition and then reuse the argument vector. For example, consider a function that that checks arbitrary 32-bit integers to see if the are sufficiently bounded:

toFinite32 :: Nat# m -> Vector n Int32# -> Maybe (Vector n (Fin32# m))

A good implementation of this function should reuse the argument as the result, and we need unsafeCoerceVector to do this.

unsafeConstruct# :: forall (a :: TYPE R) (n :: Nat). A# a -> Vector# n a Source #

This is extremely unsafe. It allows us to create a vector and invent the length. Users are not supposed to use this. It exists so that we can build with functions for arrays that support recovering the length from an array. (All array types except bit vectors support this.)

expose :: forall (n :: Nat) (a :: TYPE R). Vector n a -> A# a Source #

expose# :: forall (n :: Nat) (a :: TYPE R). Vector# n a -> A# a Source #

freezeSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s m a -> Nat# i -> Nat# n -> ST s (Vector n a) Source #

freezeSlice# :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector# s m a -> Nat# i -> Nat# n -> State# s -> (# State# s, Vector# n a #) Source #

Ranges

set Source #

Arguments

:: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a	Mutable vector
-> Nat# n	Vector length
-> a	Value
-> ST s ()

Set all elements in the mutable vector to the same value.

setSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) s (a :: TYPE R). ((i + n) <=# m) -> MutableVector s n a -> Nat# i -> Nat# m -> a -> ST s () Source #

Freeze

unsafeShrinkFreeze :: forall s (n0 :: Nat) (n1 :: Nat) (a :: TYPE R). (n1 <=# n0) -> MutableVector s n0 a -> Nat# n1 -> ST s (Vector n1 a) Source #

The argument array must not be reused.

unsafeFreeze :: forall s (n :: Nat) (a :: TYPE R). MutableVector s n a -> ST s (Vector n a) Source #

freeze Source #

Arguments

:: forall (n :: Nat) s (a :: TYPE R). Nat# n	Mutable vector length
-> MutableVector s n a	Mutable vector
-> ST s (Vector n a)

freeze# Source #

Arguments

:: forall (n :: Nat) s (a :: TYPE R). Nat# n	Mutable vector length
-> MutableVector# s n a	Mutable vector
-> State# s
-> (# State# s, Vector# n a #)

Copy

thaw Source #

Arguments

:: forall (n :: Nat) (a :: TYPE R) s. Nat# n	Vector length
-> Vector n a	Mutable vector
-> ST s (MutableVector s n a)

thawSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R) s. ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> ST s (MutableVector s n a) Source #

Composite

tail :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector (n + 1) a -> Vector n a Source #

cons :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a Source #

snoc :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> a -> Vector (n + 1) a Source #

replaceAt :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Fin# n -> a -> Vector n a Source #

empty_ :: forall (a :: TYPE R). Vector_ a Source #

map :: forall (a :: TYPE R) (n :: Nat). (a -> a) -> Vector n a -> Nat# n -> Vector n a Source #

Map over a vector starting at offset 0.

all :: forall (a :: TYPE R) (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool Source #

any :: forall (a :: TYPE R) (n :: Nat). (a -> Bool) -> Nat# n -> Vector n a -> Bool Source #

findIndex :: forall (n :: Nat) (a :: TYPE R). (a -> Bool) -> Nat# n -> Vector n a -> MaybeFin# n Source #

traverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (a -> m b) -> Nat# n -> Vector n a -> m () Source #

traverseZip_ :: forall (n :: Nat) m (a :: TYPE R) (b :: TYPE R) c. Monad m => (a -> b -> m c) -> Nat# n -> Vector n a -> Vector n b -> m () Source #

traverseST# :: forall (n :: Nat) s (a :: TYPE R) (b :: TYPE R). (a -> State# s -> (# State# s, b #)) -> Nat# n -> Vector# n a -> State# s -> (# State# s, Vector# n b #) Source #

itraverse_ :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector n a -> m () Source #

itraverse_# :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (Fin# n -> a -> m b) -> Nat# n -> Vector# n a -> m () Source #

foldlM :: forall (n :: Nat) m (a :: TYPE R) b. Monad m => (b -> a -> m b) -> b -> Nat# n -> Vector n a -> m b Source #

foldrZip :: forall (n :: Nat) (a :: TYPE R) (b :: TYPE R) c. (a -> b -> c -> c) -> c -> Nat# n -> Vector n a -> Vector n b -> c Source #

foldr :: forall (n :: Nat) (a :: TYPE R) b. (a -> b -> b) -> b -> Nat# n -> Vector n a -> b Source #

ifoldr :: forall (n :: Nat) (a :: TYPE R) b. (Fin# n -> a -> b -> b) -> b -> Nat# n -> Vector n a -> b Source #

ifoldl' :: forall (n :: Nat) (a :: TYPE R) b. (b -> Fin# n -> a -> b) -> b -> Nat# n -> Vector n a -> b Source #

ifoldlSlice' :: forall (i :: Nat) (m :: Nat) (n :: Nat) (a :: TYPE R) b. ((i + n) <= m) -> (b -> Fin# (i + n) -> a -> b) -> b -> Vector m a -> Nat# i -> Nat# n -> b Source #

liftShows :: forall (n :: Nat) (a :: TYPE R). (a -> String -> String) -> Nat# n -> Vector n a -> String -> String Source #

replicate :: forall (n :: Nat) (a :: TYPE R). Nat# n -> a -> Vector n a Source #

construct1 :: forall (a :: TYPE R). a -> Vector 1 a Source #

construct2 :: forall (a :: TYPE R). a -> a -> Vector 2 a Source #

construct3 :: forall (a :: TYPE R). a -> a -> a -> Vector 3 a Source #

construct4 :: forall (a :: TYPE R). a -> a -> a -> a -> Vector 4 a Source #

construct5 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> Vector 5 a Source #

construct6 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> Vector 6 a Source #

construct7 :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector 7 a Source #

construct1# :: forall (a :: TYPE R). a -> Vector# 1 a Source #

construct2# :: forall (a :: TYPE R). a -> a -> Vector# 2 a Source #

construct3# :: forall (a :: TYPE R). a -> a -> a -> Vector# 3 a Source #

construct4# :: forall (a :: TYPE R). a -> a -> a -> a -> Vector# 4 a Source #

construct7# :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector# 7 a Source #

construct1_ :: forall (a :: TYPE R). a -> Vector_ a Source #

construct2_ :: forall (a :: TYPE R). a -> a -> Vector_ a Source #

construct3_ :: forall (a :: TYPE R). a -> a -> a -> Vector_ a Source #

construct4_ :: forall (a :: TYPE R). a -> a -> a -> a -> Vector_ a Source #

construct7_ :: forall (a :: TYPE R). a -> a -> a -> a -> a -> a -> a -> Vector_ a Source #

append :: forall (n :: Nat) (m :: Nat) (a :: TYPE R). Nat# n -> Nat# m -> Vector n a -> Vector m a -> Vector (n + m) a Source #

clone :: forall (n :: Nat) (a :: TYPE R). Nat# n -> Vector n a -> Vector n a Source #

cloneSlice :: forall (i :: Natural) (n :: Natural) (m :: Nat) (a :: TYPE R). ((i + n) <=# m) -> Vector m a -> Nat# i -> Nat# n -> Vector n a Source #

copySlice :: forall (di :: Natural) (n :: Natural) (dn :: Nat) (si :: Natural) (sn :: Nat) s (a :: TYPE R). ((di + n) <=# dn) -> ((si + n) <=# sn) -> MutableVector s dn a -> Nat# di -> Vector sn a -> Nat# si -> Nat# n -> ST s () Source #

Index

index0 :: forall (n :: Natural) (a :: TYPE R). CmpNat 0 n ~ 'LT => Vector n a -> a Source #

index1 :: forall (n :: Natural) (a :: TYPE R). CmpNat 1 n ~ 'LT => Vector n a -> a Source #

index2 :: forall (n :: Natural) (a :: TYPE R). CmpNat 2 n ~ 'LT => Vector n a -> a Source #

index3 :: forall (n :: Natural) (a :: TYPE R). CmpNat 3 n ~ 'LT => Vector n a -> a Source #

index4 :: forall (n :: Natural) (a :: TYPE R). CmpNat 4 n ~ 'LT => Vector n a -> a Source #

index5 :: forall (n :: Natural) (a :: TYPE R). CmpNat 5 n ~ 'LT => Vector n a -> a Source #

index6 :: forall (n :: Natural) (a :: TYPE R). CmpNat 6 n ~ 'LT => Vector n a -> a Source #

index7 :: forall (n :: Natural) (a :: TYPE R). CmpNat 7 n ~ 'LT => Vector n a -> a Source #

index8 :: forall (n :: Natural) (a :: TYPE R). CmpNat 8 n ~ 'LT => Vector n a -> a Source #