| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.Exception

Description
Basically a copy of the ErrorT monad transformer. It's handy to slap onto TCM and still be a MonadTCM (which isn't possible with ErrorT).
Documentation

newtype ExceptionT err m a | Source

Constructors

ExceptionT |

runExceptionT :: m (Either err a) |

Instances

(Error err, MonadError err' m) => MonadError err' (ExceptionT err m)
(Error err, MonadReader r m) => MonadReader r (ExceptionT err m)
(Error err, MonadState s m) => MonadState s (ExceptionT err m)
(Monad m, Error err) => MonadException err (ExceptionT err m)
MonadTrans (ExceptionT err)
(Monad m, Error err) => Monad (ExceptionT err m)
Functor f => Functor (ExceptionT err f)
(Error err, Applicative m, Monad m) => Applicative (ExceptionT err m)
(Error err, MonadIO m) => MonadIO (ExceptionT err m)
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm)

class Error err => MonadException err m | m -> err where | Source

Methods

throwException :: err -> m a | Source

catchException :: m a -> (err -> m a) -> m a | Source

Instances

MonadException UnifyException Unify
MonadException UnifyException Unify
(Monad m, Error err) => MonadException err (ExceptionT err m)

Produced by Haddock version 2.4.2