fact: Definition handle_exceptT (X : UU0) (t : exceptT Z M X) (h : unit -> exceptT Z M X) : exceptT Z M X := match t with | inl z => h z | inr x => inr x end.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer imonad_model