@@ -87,6 +87,10 @@ maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
8787maybeToEither def (Just j) = Right j
8888maybeToEither def Nothing = Left def
8989
90+||| Convert an Either to a Maybe from Right injection
91+eitherToMaybe : Either e a -> Maybe a
92+eitherToMaybe (Left _) = Nothing
93+eitherToMaybe (Right x) = Just x
9094
9195--------------------------------------------------------------------------------
9296-- Implementations