fact: Definition interp_e (h : eff_hom_e) : itree E ~> itree F := fun R t => ITree.iter (fun '(s, t) => match observe t with | RetF r => Ret (inr r) | TauF t => Ret (inl (s, t)) | VisF e k => ITree.map (fun '(s, x) => inl (s, k x)) (h.(eval) _ e) end) (h, t).
imports: ExtLib(Structures.Functor Structures.Monad) ITree(Basics.Basics Basics.CategoryOps Basics.CategoryKleisli Core.ITreeDefinition Indexed.Function Indexed.Sum Core.Subevent Interp.Interp)