proposition: Lemma algebraic_handle : algebraicity handle_op.
proof: Proof. move=> A B f t. rewrite except_bindE. rewrite /handle_op /=. rewrite /handle /=. rewrite /uncurry /=. case: t => -[z//|a] g /=. rewrite except_bindE. case: (f a) => // z. rewrite /handle'. rewrite except_bindE. case: (g z) => [z0|a0]. Abort. End exceptops. Arguments throw_op {Z}. Arguments handle_op {Z}. Module StateOpsGet. Section get. Variable S : UU0. Definition acto (X : UU0) := S -> X. Let actm (X Y : UU0) (f : X -> Y) (t : acto X) : acto Y := f \o t. Let func_id : FunctorLaws.id actm. Proof. by move=> A; apply funext. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer