partitionM package:Agda

partitionM :: (Functor m, Applicative m) => (a -> m Bool) -> [a] -> m ([a], [a])

Agda Agda.Utils.Monad

A `monadic' version of @partition :: (a -> Bool) -> [a] -> ([a],[a])

partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])

Agda Agda.Utils.List

Partition a list into Nothings and Justs. O(n).

partitionMaybe f = partitionEithers . map ( a -> maybe (Left a) Right (f a))

Note: mapMaybe f = snd . partitionMaybe f.