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