Data.Vect.Ex

Definitions

mapI : (Fin n -> a -> b) -> Vect n a -> Vect n b

Totality: total
Visibility: public export

toListI : Vect n a -> List (a, Fin n)

Totality: total
Visibility: export

withIndex : Vect n a -> Vect n (Fin n, a)

Totality: total
Visibility: export

drop'' : Vect n a -> (count : Fin (S n)) -> Vect (n - count) a

Totality: total
Visibility: public export

mapPre : ((i : Fin n) -> Vect (finToNat i) b -> a -> b) -> Vect n a -> Vect n b

Totality: total
Visibility: export

fromMap : SortedMap (Fin n) a -> Vect n (Maybe a)

Totality: total
Visibility: export

presenceVect : SortedSet (Fin n) -> Vect n Bool

Totality: total
Visibility: export

reverseMapping : Ord a => Vect n a -> SortedMap a (List1 (Fin n))

Totality: total
Visibility: public export