Data.Vect.Dependent

Definitions

data DVect : (n : Nat) -> (Fin n -> Type) -> Type

Totality: total
Visibility: public export
Constructors:

Nil : DVect 0 ty

(::) : ty FZ -> DVect n (ty . FS) -> DVect (S n) ty

Hints:

Eq (a i) => Eq (DVect n a)

Monoid (a i) => Monoid (DVect n a)

Ord (a i) => Ord (DVect n a)

Semigroup (a i) => Semigroup (DVect n a)

Show (a i) => Show (DVect n a)

index : (i : Fin n) -> DVect n a -> a i

Totality: total
Visibility: public export

tabulateI : ((i : Fin n) -> a i) -> DVect n a

Totality: total
Visibility: public export

tabulate : a i -> DVect n a

Totality: total
Visibility: public export

(++) : DVect n a -> DVect m b -> DVect (n + m) (either (Delay a) (Delay b) . splitSum)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

replaceAt : (i : Fin n) -> a i -> DVect n a -> DVect n a

Totality: total
Visibility: public export

updateAt : (i : Fin n) -> (a i -> a i) -> DVect n a -> DVect n a

Totality: total
Visibility: public export

mapI : ((i : Fin n) -> a i -> b i) -> DVect n a -> DVect n b

Totality: total
Visibility: public export

map : (a i -> b i) -> DVect n a -> DVect n b

Totality: total
Visibility: public export

(<$>) : (a i -> b i) -> DVect n a -> DVect n b

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 4

(<&>) : DVect n a -> (a i -> b i) -> DVect n b

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1

mapPreI : ((i : Fin n) -> DVect (finToNat i) (b . weakenToSuper) -> a i -> b i) -> DVect n a -> DVect n b

Totality: total
Visibility: public export

mapPre : (DVect (finToNat i) (b . weakenToSuper) -> a i -> b i) -> DVect n a -> DVect n b

Totality: total
Visibility: public export

downmapI : ((i : Fin n) -> a i -> b) -> DVect n a -> Vect n b

Totality: total
Visibility: public export

downmap : (a i -> b) -> DVect n a -> Vect n b

Totality: total
Visibility: public export

upmapI : ((i : Fin n) -> a -> b i) -> Vect n a -> DVect n b

Totality: total
Visibility: public export

upmap : (a -> b i) -> Vect n a -> DVect n b

Totality: total
Visibility: public export

zip : DVect n a -> DVect n b -> DVect n (\i => (a i, b i))

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

zipWithI : ((i : Fin n) -> a i -> b i -> c i) -> DVect n a -> DVect n b -> DVect n c

Totality: total
Visibility: public export

zipWith : (a i -> b i -> c i) -> DVect n a -> DVect n b -> DVect n c

Totality: total
Visibility: public export

(<*>) : DVect n (\i => a i -> b i) -> DVect n a -> DVect n b

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3

transpose : {0 a : Fin n -> Fin m -> Type} -> DVect n (\i => DVect m (\j => a i j)) -> DVect m (\j => DVect n (\i => a i j))

Totality: total
Visibility: public export

foldlI : ((i : Fin n) -> acc -> a i -> acc) -> acc -> DVect n a -> acc

Totality: total
Visibility: public export

foldl : (acc -> a i -> acc) -> acc -> DVect n a -> acc

Totality: total
Visibility: public export

foldrI : ((i : Fin n) -> a i -> Lazy acc -> acc) -> acc -> DVect n a -> acc

Totality: total
Visibility: public export

foldr : (a i -> Lazy acc -> acc) -> acc -> DVect n a -> acc

Totality: total
Visibility: public export

foldlMI : Monad m => ((i : Fin n) -> acc -> a i -> m acc) -> acc -> DVect n a -> m acc

Totality: total
Visibility: public export

foldlM : Monad m => (acc -> a i -> m acc) -> acc -> DVect n a -> m acc

Totality: total
Visibility: public export

traverseI : Applicative f => ((i : Fin n) -> a i -> f (b i)) -> DVect n a -> f (DVect n b)

Totality: total
Visibility: public export

traverse : Applicative f => (a i -> f (b i)) -> DVect n a -> f (DVect n b)

Totality: total
Visibility: public export

sequence : Applicative f => DVect n (f . a) -> f (DVect n a)

Totality: total
Visibility: public export

forI : Applicative f => DVect n a -> ((i : Fin n) -> a i -> f (b i)) -> f (DVect n b)

Totality: total
Visibility: public export

for : Applicative f => DVect n a -> (a i -> f (b i)) -> f (DVect n b)

Totality: total
Visibility: public export