Idris2Doc : Control.Effect.Exception

Control.Effect.Exception

(source)
Reexports
import public Control.Effect.Fail
Definitions
data TryE : Type -> (Type -> Type) -> Type -> Type
  Exception effect.

  Totality: total
  Visibility: public export
  Constructor: 
Try : m a -> (e -> m a) -> TryE e m a

  Hints:
  
Contravariant (\e => TryE e m r)
  
Inj (EitherE e) sig => Inj (TryE e) sig
EitherE : Type -> (Type -> Type) -> Type -> Type
  Visibility: public export
try : Inj (TryE e) sig => Algebra sig m => m a -> (e -> m a) -> m a
  Try running a computation. If it fails (via Fail) resort to the supplied callback.

  Visibility: public export
AlgebraEither : Algebra sig m => Algebra (EitherE e :+: sig) (EitherT e m)
  Visibility: public export