fact: Definition _interp_mrec {R : Type} (ot : itreeF (D +' E) R _) : itree E R := match ot with | RetF r => Ret r | TauF t => Tau (interp_mrec ctx t) | VisF e k => match e with | inl1 d => Tau (interp_mrec ctx (ctx _ d >>= k)) | inr1 e => Vis e (fun x => Tau (interp_mrec ctx (k x))) end end.
imports: Paco.paco Coq(Program.Tactics Setoid Morphisms) ITree(Basics.Utils Basics.Category Basics.Basics Basics.Function Core.ITreeDefinition Core.KTree Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Handler Interp.Interp Interp.InterpFacts Interp.Recursion)