@@ -372,14 +372,11 @@ find p (x::xs) with (p x)
372372 | False = find p xs
373373
374374||| Find the index of the first element of the vector that satisfies some test
375−findIndex : (a -> Bool) -> Vect n a -> Maybe Nat
376−findIndex = findIndex' 0
377− where
378− findIndex' : Nat -> (a -> Bool) -> Vect n a -> Maybe Nat
379− findIndex' cnt p [] = Nothing
380− findIndex' cnt p (x::xs) with (p x)
381− | True = Just cnt
382− | False = findIndex' (S cnt) p xs
375+findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
376+findIndex p [] = Nothing
377+findIndex p (x :: xs) with (p x)
378+ | True = Just 0
379+ | False = map FS (findIndex p xs)
383380
384381||| Find the indices of all elements that satisfy some test
385382total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
@@ -394,10 +391,10 @@ findIndices = findIndices' 0
394391 else
395392 (_ ** tail)
396393
397−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe Nat
394+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
398395elemIndexBy p e = findIndex $ p e
399396
400−elemIndex : Eq a => a -> Vect m a -> Maybe Nat
397+elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
401398elemIndex = elemIndexBy (==)
402399
403400total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)