@@ -434,11 +434,17 @@ runPureInit env prog = eff env prog (\r, env => r)
434434runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
435435runWith inj env prog = eff env prog (\r, env => inj r)
436436
437+||| Similar to 'runInit', but take the result of `Env`.
437438%no_implicit
438439runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
439440 m (x : a ** Env m (xs' x))
440441runEnv env prog = eff env prog (\r, env => pure (r ** env))
441442
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+
442448-- ----------------------------------------------- [ some higher order things ]
443449
444450mapE : (a -> EffM m b xs (\_ => xs)) -> List a -> EffM m (List b) xs (\_ => xs)