fact: Definition _interp_fail {E F R} (f : E ~> failT (itree F)) (ot : itreeF E R _) : failT (itree F) R := match ot with | RetF r => ret r | TauF t => Tau (interp_fail f t) | VisF e k => bind (f _ e) (fun x => Tau (interp_fail f (k x))) end.
imports: Coq(Morphisms) Paco(paco) ITree(Basics.Utils Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts)