@@ -369,17 +369,10 @@ findIndex p [] = Nothing
369369findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
370370
371371||| Find the indices of all elements that satisfy some test
372−findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
373−findIndices = findIndices' 0
374− where
375− total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
376− findIndices' cnt p [] = (_ ** [])
377− findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)
378− | (_ ** tail) =
379− if p x then
380− (_ ** cnt::tail)
381− else
382− (_ ** tail)
372+findIndices : (a -> Bool) -> Vect m a -> List (Fin m)
373+findIndices p [] = []
374+findIndices p (x :: xs) = let is = map FS $ findIndices p xs
375+ in if p x then 0 :: is else is
383376
384377elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
385378elemIndexBy p e = findIndex $ p e
@@ -387,10 +380,10 @@ elemIndexBy p e = findIndex $ p e
387380elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
388381elemIndex = elemIndexBy (==)
389382
390−elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
383+elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)
391384elemIndicesBy p e = findIndices $ p e
392385
393−elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
386+elemIndices : Eq a => a -> Vect m a -> List (Fin m)
394387elemIndices = elemIndicesBy (==)
395388
396389--------------------------------------------------------------------------------