fact: Definition choose {E} `{nondetE -< E} `{exceptE no_choice -< E} {X} : list X -> itree E X := fix choose' xs : itree E X := match xs with | [] => throw NoChoice | x :: xs => or (Ret x) (choose' xs) end.
imports: Coq(List) ITree(Basics.Basics Core.ITreeDefinition Indexed.Sum Core.Subevent Events.Exception)