@@ -252,13 +252,14 @@ eff {xs = [l ::: x]} env (l :- prog) k
253-- yuck :) Haven't got type class instances working nicely in tactic
253-- yuck :) Haven't got type class instances working nicely in tactic
254-- proofs yet, so just brute force it.
254-- proofs yet, so just brute force it.
255+syntax MkDefaultEnv = with Env
255−syntax MkDefaultEnv = (| [], [default], [default, default],
256+ (| [], [default], [default, default],
256− [default, default, default],
257+ [default, default, default],
257− [default, default, default, default],
258+ [default, default, default, default],
258− [default, default, default, default, default],
259+ [default, default, default, default, default],
259− [default, default, default, default, default, default],
260+ [default, default, default, default, default, default],
260− [default, default, default, default, default, default, default],
261+ [default, default, default, default, default, default, default],
261− [default, default, default, default, default, default, default, default] |)
262+ [default, default, default, default, default, default, default, default] |)
263run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
264run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
264run {env} prog = eff env prog (\r, env => pure r)
265run {env} prog = eff env prog (\r, env => pure r)