Idris2Doc : Control.Monad.Maybe

Control.Monad.Maybe

Definitions

dataMaybeT : (Type->Type) ->Type->Type
  A monad transformer extending an inner monad with the ability to not return
a result.

Sequenced actions produce a result only if both actions return a result.

`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: 
MkMaybeT : m (Maybea) ->MaybeTma

Hints:
Monadm=>Alternative (MaybeTm)
Applicativem=>Applicative (MaybeTm)
Eq (m (Maybea)) =>Eq (MaybeTma)
Foldablem=>Foldable (MaybeTm)
Functorm=>Functor (MaybeTm)
HasIOm=>HasIO (MaybeTm)
Monadm=>Monad (MaybeTm)
Monadm=>MonadError () (MaybeTm)
MonadErrorem=>MonadErrore (MaybeTm)
MonadTransMaybeT
Monadm=>Monoid (MaybeTma)
Ord (m (Maybea)) =>Ord (MaybeTma)
Monadm=>Semigroup (MaybeTma)
Show (m (Maybea)) =>Show (MaybeTma)
Traversablem=>Traversable (MaybeTm)
runMaybeT : MaybeTma->m (Maybea)
  Unwrap a `MaybeT` computation.

Totality: total
Visibility: public export
isNothingT : Functorm=>MaybeTma->mBool
  Check if a monadic computation returns a result. This returns `False` if
the computation returns a result, and `True` otherwise.

This is a version of `isNothing` lifted to work with `MaybeT`.

Totality: total
Visibility: public export
isJustT : Functorm=>MaybeTma->mBool
  Check if a monadic computation returns a result. This returns `True` if
the computation returns a result, and `False` otherwise.

This is a version of `isJust` lifted to work with `MaybeT`.

Totality: total
Visibility: public export
maybeT : Monadm=>mb-> (a->mb) ->MaybeTma->mb
  Run a `MaybeT` computation, handling the case of a result or no result
seperately.

This is a version of `maybe` lifted to work with `MaybeT`.

Totality: total
Visibility: public export
fromMaybeT : Monadm=>ma->MaybeTma->ma
  Run a `MaybeT` computation providing a default value.

This is a version of `fromMaybe` lifted to work with `MaybeT`.

Totality: total
Visibility: public export
toMaybeT : Functorm=>Bool->ma->MaybeTma
  Return a value if a condition is met, or else no value.

This is a version of `toMaybe` lifted to work with `MaybeT`.

Totality: total
Visibility: public export
mapMaybeT : (m (Maybea) ->n (Maybea')) ->MaybeTma->MaybeTna'
  Map over the underlying computation.

Totality: total
Visibility: public export
just : Applicativem=>a->MaybeTma
  A version of `Just` lifted to work with `MaybeT`.

This is equivalent to `pure`.

Totality: total
Visibility: public export
nothing : Applicativem=>MaybeTma
  A version of `Nothing` lifted to work with `MaybeT`.

This is equivalent to `throwE ()`.

Totality: total
Visibility: public export