@@ -440,6 +440,11 @@ runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
440440 m (x : a ** Env m (xs' x))
441441runEnv env prog = eff env prog (\r, env => pure (r ** env))
442442
443+||| Similar to 'runEnv', but the context (m) is 'pure'
444+%no_implicit
445+runPureEnv : (env : Env Basics.id xs) -> (prog : EffM Basics.id a xs xs') -> (x : a ** Env Basics.id (xs' x))
446+runPureEnv env prog = eff env prog (\r, env => (r ** env))
447+
443448-- ----------------------------------------------- [ some higher order things ]
444449
445450mapE : (a -> EffM m b xs (\_ => xs)) -> List a -> EffM m (List b) xs (\_ => xs)