Either package:Agda

eitherDecode :: FromJSON a => ByteString -> Either String a

Disjoint sum of three.

eitherDecode' :: FromJSON a => ByteString -> Either String a

Like decode but returns an error message when decoding fails.

eitherDecodeFileStrict :: FromJSON a => FilePath -> IO (Either String a)

Like decode' but returns an error message when decoding fails. Since 2.2.0.0 an alias for eitherDecode.

eitherDecodeFileStrict' :: FromJSON a => FilePath -> IO (Either String a)

Like decodeFileStrict but returns an error message when decoding fails.

eitherDecodeStrict :: FromJSON a => ByteString -> Either String a

Like decodeFileStrict' but returns an error message when decoding fails. Since 2.2.0.0 an alias for eitherDecodeFileStrict'.

eitherDecodeStrict' :: FromJSON a => ByteString -> Either String a

Like decodeStrict but returns an error message when decoding fails.

eitherDecodeStrictText :: FromJSON a => Text -> Either String a

Like decodeStrict' but returns an error message when decoding fails. Since 2.2.0.0 an alias for eitherDecodeStrict.

unblockOnEither :: Blocker -> Blocker -> Blocker

Like decodeStrictText but returns an error message when decoding fails.

Agda Agda.Syntax.Internal.Blockers

ChooseEither :: FlexChoice

Agda Agda.TypeChecking.Rules.LHS.Problem

caseEitherM :: Monad m => m (Either a b) -> (a -> m c) -> (b -> m c) -> m c

groupByEither :: forall a b . [Either a b] -> [Either (List1 a) (List1 b)]

Monadic version of either with a different argument ordering.

maybeToEither :: e -> Maybe a -> Either e a

Groups a list into alternating chunks of Left and Right values

swapEither :: Either a b -> Either b a

Convert Maybe to Either e, given an error e for the Nothing case.

traverseEither :: Functor f => (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)

Swap tags Left and Right.

partitionEithers :: List1 (Either a b) -> ([a], [b])

Either is bitraversable. Note: From base >= 4.10.0.0 already present in Bitraversable.

Agda Agda.Utils.List1

Like partitionEithers.

fromList1Either :: List1 a -> Either a (List2 a)

Agda Agda.Utils.List2

Any List1 is either a singleton or a List2. O(1).

toList1Either :: Either a (List2 a) -> List1 a

Agda Agda.Utils.List2

Inverse of fromList1Either. O(1).

orEitherM :: (Monoid e, Monad m, Functor m) => [m (Either e b)] -> m (Either e b)

Agda Agda.Utils.Monad

Lazy monadic disjunction with accumulation of errors in a monoid. Errors are discarded if we succeed.

forEither3M :: Applicative m => [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])

mapEither3M :: Applicative m => (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])

partitionEithers3 :: [Either3 a b c] -> ([a], [b], [c])