@@ -434,6 +434,7 @@ runPureInit env prog = eff env prog (\r, env => r)
434runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
434runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
435runWith inj env prog = eff env prog (\r, env => inj r)
435runWith inj env prog = eff env prog (\r, env => inj r)
437+||| Similar to 'runInit', but take the result of `Env`.
437%no_implicit
438%no_implicit
438runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
439runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
439 m (x : a ** Env m (xs' x))
440 m (x : a ** Env m (xs' x))