Control.Eff.Except

Definitions

data ExceptL : k -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

Err : err -> ExceptL lbl err a

Except : Type -> Type -> Type

Totality: total
Visibility: public export

FailL : k -> Type -> Type

Totality: total
Visibility: public export

Fail : Type -> Type

Totality: total
Visibility: public export

throwAt : (0 lbl : k) -> Has (ExceptL lbl err) fs => err -> Eff fs a

Totality: total
Visibility: export

throw : Has (Except err) fs => err -> Eff fs a

Totality: total
Visibility: export

failAt : (0 lbl : k) -> Has (FailL lbl) fs => Eff fs a

Totality: total
Visibility: export

fail : Has Fail fs => Eff fs a

Totality: total
Visibility: export

rethrowAt : (0 lbl : k) -> Has (ExceptL lbl err) fs => Either err a -> Eff fs a

Totality: total
Visibility: export

rethrow : Has (Except err) fs => Either err a -> Eff fs a

Totality: total
Visibility: export

noteAt : (0 lbl : k) -> Has (ExceptL lbl err) fs => Lazy err -> Maybe a -> Eff fs a

Totality: total
Visibility: export

note : Has (Except err) fs => Lazy err -> Maybe a -> Eff fs a

Totality: total
Visibility: export

fromJustAt : (0 lbl : k) -> Has (FailL lbl) fs => Maybe a -> Eff fs a

Totality: total
Visibility: export

fromJust : Has Fail fs => Maybe a -> Eff fs a

Totality: total
Visibility: export

catchAt : (0 lbl : k) -> {auto {conArg:2308} : Has (ExceptL lbl err) fs} -> (err -> Eff (fs - ExceptL lbl err) a) -> Eff fs a -> Eff (fs - ExceptL lbl err) a

Totality: total
Visibility: export

catch : {auto {conArg:2391} : Has (Except err) fs} -> (err -> Eff (fs - Except err) a) -> Eff fs a -> Eff (fs - Except err) a

Totality: total
Visibility: export

runExceptAt : (0 lbl : k) -> {auto {conArg:2444} : Has (ExceptL lbl err) fs} -> Eff fs a -> Eff (fs - ExceptL lbl err) (Either err a)

Totality: total
Visibility: export

runExcept : {auto {conArg:2522} : Has (Except err) fs} -> Eff fs a -> Eff (fs - Except err) (Either err a)

Totality: total
Visibility: export

runFailAt : (0 lbl : k) -> {auto {conArg:2559} : Has (FailL lbl) fs} -> Eff fs a -> Eff (fs - FailL lbl) (Maybe a)

Totality: total
Visibility: export

runFail : {auto {conArg:2621} : Has Fail fs} -> Eff fs a -> Eff (fs - Fail) (Maybe a)

Totality: total
Visibility: export