@@ -171,7 +171,7 @@ data Eff : (m : Type -> Type) ->
171171
172172 lift : (prf : SubList ys xs) ->
173173 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 =>
175175 res ->
176176 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
177177 Eff m a xs (\v => xs')
@@ -226,7 +226,7 @@ eff env (effect prf effP) k = execEff env prf effP k
226226eff env (lift prf effP) k
227227 = let env' = dropEnv env prf in
228228 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
230230 = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)
231231eff env (catch prog handler) k
232232 = catch (eff env prog k)
@@ -265,6 +265,11 @@ effect' : {a, b: _} -> {e : Effect} ->
265265 Eff m t xs (\v => updateResTy v xs prf eff)
266266effect' e {prf} = effect prf e
267267
268+new : Handler e m =>
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
268273
269274run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
270275run {env} prog = eff env prog (\r, env => pure r)