module Data.Either ||| True if the argument is Left, False otherwisepublic exportisLeft : Either a b -> BoolisLeft (Left l)  = TrueisLeft (Right r) = False ||| True if the argument is Right, False otherwisepublic exportisRight : Either a b -> BoolisRight (Left l)  = FalseisRight (Right r) = True ||| Keep the payloads of all Left constructors in a list of Eitherspublic exportlefts : List (Either a b) -> List alefts []      = []lefts (x::xs) =  case x of    Left  l => l :: lefts xs    Right r => lefts xs ||| Keep the payloads of all Right constructors in a list of Eitherspublic exportrights : List (Either a b) -> List brights []      = []rights (x::xs) =  case x of    Left  l => rights xs    Right r => r :: rights xs ||| Split a list of Eithers into a list of the left elements and a list of the right elementspublic exportpartitionEithers : List (Either a b) -> (List a, List b)partitionEithers l = (lefts l, rights l) ||| Remove a "useless" Either by collapsing the case distinctionpublic exportfromEither : Either a a -> afromEither (Left l)  = lfromEither (Right r) = r ||| Right becomes left and left becomes rightpublic exportmirror : Either a b -> Either b amirror (Left  x) = Right xmirror (Right x) = Left x ---------------------------------------------------------------------------------- Conversions-------------------------------------------------------------------------------- ||| Convert a Maybe to an Either by using a default value in case of Nothing||| @ e the default valuepublic exportmaybeToEither : (def : Lazy e) -> Maybe a -> Either e amaybeToEither def (Just j) = Right jmaybeToEither def Nothing  = Left  def ||| Convert an Either to a Maybe from Right injectionpublic exporteitherToMaybe : Either e a -> Maybe aeitherToMaybe (Left _) = NothingeitherToMaybe (Right x) = Just x  -- Injectivity of constructors ||| Left is injectivetotalleftInjective : {b : Type}             -> {x : a}             -> {y : a}             -> (Left {b = b} x = Left {b = b} y) -> (x = y)leftInjective Refl = Refl ||| Right is injectivetotalrightInjective : {a : Type}              -> {x : b}              -> {y : b}              -> (Right {a = a} x = Right {a = a} y) -> (x = y)rightInjective Refl = Refl