@@ -369,17 +369,10 @@ findIndex p [] = Nothing
369findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
369findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
371||| Find the indices of all elements that satisfy some test
371||| Find the indices of all elements that satisfy some test
372−findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
372+findIndices : (a -> Bool) -> Vect m a -> List (Fin m)
373−findIndices = findIndices' 0
375− total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
376− findIndices' cnt p [] = (_ ** [])
373+findIndices p [] = []
377− findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)
374+findIndices p (x :: xs) = let is = map FS $ findIndices p xs
379− if p x then
375+ in if p x then 0 :: is else is
384elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
377elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
385elemIndexBy p e = findIndex $ p e
378elemIndexBy p e = findIndex $ p e
@@ -387,10 +380,10 @@ elemIndexBy p e = findIndex $ p e
387elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
380elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
388elemIndex = elemIndexBy (==)
381elemIndex = elemIndexBy (==)
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)
391elemIndicesBy p e = findIndices $ p e
384elemIndicesBy p e = findIndices $ p e
393−elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
386+elemIndices : Eq a => a -> Vect m a -> List (Fin m)
394elemIndices = elemIndicesBy (==)
387elemIndices = elemIndicesBy (==)
396--------------------------------------------------------------------------------
389--------------------------------------------------------------------------------