fact: Definition handle_map {E} : mapE ~> stateT map (itree E) := fun _ e env => match e with | Insert k v => Ret (Maps.add k v env, tt) | Lookup k => Ret (env, Maps.lookup k env) | Remove k => Ret (Maps.remove k env, tt) end.
imports: Coq(List) ITree(Basics.Basics Basics.CategoryOps Basics.MonadState Indexed.Sum Core.ITreeDefinition Core.Subevent Interp.Interp Events.State)