Idris2Doc : Control.Monad.Error.Either

Control.Monad.Error.Either

Provides a monad transformer `EitherT` that extends an inner monad with the
ability to throw and catch exceptions.

Definitions

dataEitherT : Type-> (Type->Type) ->Type->Type
  A monad transformer extending an inner monad with the ability to throw and
catch exceptions.

Sequenced actions produce an exception if either action produces an
exception, with preference for the first exception. If neither produce an
exception, neither does the sequence of actions.

`MaybeT m a` is equivalent to `EitherT () m a`, that is, an computation
that can only throw a single, information-less exception.

Totality: total
Visibility: public export
Constructor: 
MkEitherT : m (Eitherea) ->EitherTema

Hints:
(Monadm, Monoide) =>Alternative (EitherTem)
Applicativem=>Applicative (EitherTem)
Eq (m (Eitherea)) =>Eq (EitherTema)
Foldablem=>Foldable (EitherTem)
Functorm=>Functor (EitherTem)
HasIOm=>HasIO (EitherTem)
Monadm=>Monad (EitherTem)
Monadm=>MonadErrore (EitherTem)
MonadTrans (EitherTe)
Ord (m (Eitherea)) =>Ord (EitherTema)
Monadm=>Semigroup (EitherTema)
Show (m (Eitherea)) =>Show (EitherTema)
Traversablem=>Traversable (EitherTem)
runEitherT : EitherTema->m (Eitherea)
  Unwrap an `EitherT` computation.

Totality: total
Visibility: public export
eitherT : Monadm=> (a->mc) -> (b->mc) ->EitherTamb->mc
  Run an `EitherT` computation, handling results and exceptions with seperate
functions.

This is a version of `either` lifted to work with `EitherT`.

Totality: total
Visibility: public export
mapEitherT : (m (Eitherea) ->n (Eithere'a')) ->EitherTema->EitherTe'na'
  Map over the underlying monadic computation.

Totality: total
Visibility: public export
bimapEitherT : Functorm=> (a->c) -> (b->d) ->EitherTamb->EitherTcmd
  Map over the result or the exception of a monadic computation.

Totality: total
Visibility: public export
left : Applicativem=>e->EitherTema
  A version of `Left` lifted to work with `EitherT`.

This is equivalent to `throwE`.

Totality: total
Visibility: public export
right : Applicativem=>a->EitherTema
  A version of `Right` lifted to work with `EitherT`.

This is equivalent to `pure`.

Totality: total
Visibility: public export
swapEitherT : Functorm=>EitherTema->EitherTame
  Swap the result and the exception of a monadic computation.

Totality: total
Visibility: public export
throwE : Applicativem=>e->EitherTema
  Throw an exception in a monadic computation.

Totality: total
Visibility: public export
catchE : Monadm=>EitherTema-> (e->EitherTe'ma) ->EitherTe'ma
  Handle an exception thrown in a monadic computation.

Since the handler catches all errors thrown in the computation, it may
raise a different exception type.

Totality: total
Visibility: public export