Data.Vect.Extra1

Move these to stdlib Data.Vect.Extra

Definitions

mapWithPosTabulate : (f : (Fin n -> a -> b)) -> (x : a) -> mapWithPos f (replicate n x) = tabulate (flip f x)

Totality: total
Visibility: export

mapWithPosAsTabulate : (f : (Fin n -> a -> b)) -> (xs : Vect n a) -> mapWithPos f xs = tabulate (\i => f i (index i xs))

Totality: total
Visibility: export

mapWithPosIrrelevant : ((0 _ : Fin n) -> a -> b) -> Vect n a -> Vect n b

  Version of `map` with runtime-irrelevant access to the current position

Totality: total
Visibility: public export

mapWithPosFusion : (f : (Fin n -> b -> c)) -> (g : (a -> b)) -> (xs : Vect n a) -> mapWithPos f (map g xs) = mapWithPos (\i => f i . g) xs

Totality: total
Visibility: export

indexIndexSumLeft : (p : Fin m) -> index (indexSum (Left p)) (xs ++ ys) = index p xs

Totality: total
Visibility: export

indexIndexSumRight : (0 p : Fin n) -> index (indexSum (Right p)) (xs ++ ys) = index p ys

Totality: total
Visibility: export