@@ -171,7 +171,7 @@ data Eff : (m : Type -> Type) ->
172 lift : (prf : SubList ys xs) ->
172 lift : (prf : SubList ys xs) ->
173 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
173 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
174− new : Handler e m =>
174+ newInit : Handler e m =>
176 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
176 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
177 Eff m a xs (\v => xs')
177 Eff m a xs (\v => xs')
@@ -226,7 +226,7 @@ eff env (effect prf effP) k = execEff env prf effP k
226eff env (lift prf effP) k
226eff env (lift prf effP) k
227 = let env' = dropEnv env prf in
227 = let env' = dropEnv env prf in
228 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
228 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
229−eff env (new r prog) k
229+eff env (newInit r prog) k
230 = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)
230 = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)
231eff env (catch prog handler) k
231eff env (catch prog handler) k
232 = catch (eff env prog k)
232 = catch (eff env prog k)
@@ -265,6 +265,11 @@ effect' : {a, b: _} -> {e : Effect} ->
265 Eff m t xs (\v => updateResTy v xs prf eff)
265 Eff m t xs (\v => updateResTy v xs prf eff)
266effect' e {prf} = effect prf e
266effect' e {prf} = effect prf e
269+ {default default r : res} ->
270+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
271+ Eff m a xs (\v => xs')
272+new {r} e = newInit r e
269run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
274run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
270run {env} prog = eff env prog (\r, env => pure r)
275run {env} prog = eff env prog (\r, env => pure r)