@@ -372,14 +372,11 @@ find p (x::xs) with (p x)
372 | False = find p xs
372 | False = find p xs
374||| Find the index of the first element of the vector that satisfies some test
374||| Find the index of the first element of the vector that satisfies some test
375−findIndex : (a -> Bool) -> Vect n a -> Maybe Nat
375+findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
376−findIndex = findIndex' 0
378− findIndex' : Nat -> (a -> Bool) -> Vect n a -> Maybe Nat
379− findIndex' cnt p [] = Nothing
376+findIndex p [] = Nothing
380− findIndex' cnt p (x::xs) with (p x)
377+findIndex p (x :: xs) with (p x)
381− | True = Just cnt
378+ | True = Just 0
382− | False = findIndex' (S cnt) p xs
379+ | False = map FS (findIndex p xs)
384||| Find the indices of all elements that satisfy some test
381||| Find the indices of all elements that satisfy some test
385total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
382total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
@@ -394,10 +391,10 @@ findIndices = findIndices' 0
395 (_ ** tail)
392 (_ ** tail)
397−elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe Nat
394+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
398elemIndexBy p e = findIndex $ p e
395elemIndexBy p e = findIndex $ p e
400−elemIndex : Eq a => a -> Vect m a -> Maybe Nat
397+elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
401elemIndex = elemIndexBy (==)
398elemIndex = elemIndexBy (==)
403total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
400total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)