[ cleanup ] Small code cleanup, less mutual block and one \case use

Author: buzden

libs/base/Data/Either.idr

@@ -34,20 +34,16 @@ isRight (Right _) = True
 --------------------------------------------------------------------------------
 -- Grouping values
 
-mutual
-
-  ||| Compress the list of Lefts and Rights by accumulating
-  ||| all of the lefts and rights into non-empty blocks.
-  export
-  compress : List (Either a b) -> List (Either (List1 a) (List1 b))
-  compress [] = []
-  compress (Left a :: abs) = compressLefts (singleton a) abs
-  compress (Right b :: abs) = compressRights (singleton b) abs
-
+||| Compress the list of Lefts and Rights by accumulating
+||| all of the lefts and rights into non-empty blocks.
+export
+compress : List (Either a b) -> List (Either (List1 a) (List1 b))
+compress [] = []
+compress (Left x :: abs) = compressLefts (singleton x) abs where
   compressLefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
   compressLefts acc (Left a :: abs) = compressLefts (cons a acc) abs
   compressLefts acc abs = Left (reverse acc) :: compress abs
-
+compress (Right y :: abs) = compressRights (singleton y) abs where
   compressRights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
   compressRights acc (Right b :: abs) = compressRights (cons b acc) abs
   compressRights acc abs = Right (reverse acc) :: compress abs
@@ -56,8 +52,8 @@ mutual
 ||| right inverse because nothing forces the input to be maximally compressed!
 export
 decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)
-decompress = concatMap $ \ abs => case abs of
-  Left as => map Left  $ forget as
+decompress = concatMap $ \case
+  Left  as => map Left  $ forget as
   Right bs => map Right $ forget bs
 
 ||| Keep the payloads of all Left constructors in a list of Eithers