fact: Definition handle_map {E d} : mapE d ~> stateT map (itree E) := fun _ e env => match e with | Insert k v => Ret (Maps.add k v env, tt) | LookupDef k => Ret (env, lookup_default k d env) | Remove k => Ret (Maps.remove k env, tt) end.
imports: ExtLib(Core.RelDec) ITree(Basics.Basics Basics.CategoryOps Basics.CategoryKleisli Basics.Monad Indexed.Function Indexed.Sum Core.ITreeDefinition Core.Subevent Interp.Interp Interp.Handler Events.State)