fact: Definition _interp {E F R} (f : E ~> itree F) (ot : itreeF E R _) : itree F R := match ot with | RetF r => Ret r | TauF t => Tau (interp f t) | VisF e k => f _ e >>= (fun x => Tau (interp f (k x))) end.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp Interp.Handler Interp.TranslateFacts)