@@ -249,15 +249,13 @@ syntax MkDefaultEnv = with Env
250call : {a, b: _} -> {e : Effect} ->
250call : {a, b: _} -> {e : Effect} ->
251 (eff : e t a b) ->
251 (eff : e t a b) ->
252− {default tactics { search 100; }
253− prf : EffElem e a xs} ->
252+ {auto prf : EffElem e a xs} ->
254 Eff m t xs (\v => updateResTy v xs prf eff)
253 Eff m t xs (\v => updateResTy v xs prf eff)
255call e {prf} = callP prf e
254call e {prf} = callP prf e
258lift : Eff m t ys ys' ->
257lift : Eff m t ys ys' ->
259− {default tactics { search 100; }
260− prf : SubList ys xs} ->
258+ {auto prf : SubList ys xs} ->
261 Eff m t xs (\v => updateWith (ys' v) xs prf)
259 Eff m t xs (\v => updateWith (ys' v) xs prf)
262lift e {prf} = liftP prf e
260lift e {prf} = liftP prf e